Theorem mpancom 704

Description: An inference based on modus ponens with commutation of antecedents.

Hypotheses

Ref	Expression
mpancom.1	|- (ps -> ph)
mpancom.2	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
mpancom	|- (ps -> ch)

Proof of Theorem mpancom

Step	Hyp	Ref	Expression
1		mpancom.1	. 2 |- (ps -> ph)
2		mpancom.2	. . 3 |- ((ph /\ ps) -> ch)
3	2	ancoms 436	. 2 |- ((ps /\ ph) -> ch)
4	1, 3	mpdan 703	1 |- (ps -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  reuuni3 2881  orduniorsuc 3082  unielxp 4097  fodomfi 4546  pwfilem 4550  cardnn 4804  ondomcard 4837  ltexprlem4 5125  ledivp1 5862  ltdivp1 5863  flidt 6188  eluzfzt 6417  seqzcl 6498  crret 6710  crretOLD 6711  crimt 6712  crimtOLD 6713  faclbnd3 6892  faclbnd4lem4 6896  bcxmaslem1 7020  caucvg3lem 7110  eftlubclt 7326  issubgi 8074  ablmul 8083  vcoprnelem 8149  htthlem9 8571  circgrpOLD 8677  hilabl 8966  mayete3 9613  homulid2t 9666  lnopeq 9871  cnlnadjlem7 9944  adjbdlnb 9955  nmopcoadj 9972  bracnlnvalt 9985  hmopidmchlem 10016  hmopidmch 10017  hmopidmpj 10018  symggrpi 10340

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain