Theorem mpancom 418

Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

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		id 19	. 2 |- ( ps -> ps )
3		mpancom.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	1, 2, 3	syl2anc 408	1 |- ( ps -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mpan  420  spesbc  2989  onsucelsucr  4419  sucunielr  4421  ordsuc  4473  peano2b  4523  xpiindim  4671  fvelrnb  5462  fliftcnv  5689  riotaprop  5746  unielxp  6065  dmtpos  6146  tpossym  6166  ercnv  6443  cnvct  6696  php5dom  6750  3xpfi  6812  recrecnq  7195  1idpr  7393  eqlei2  7851  lem1  8598  eluzfz1  9804  fzpred  9843  uznfz  9876  fz0fzdiffz0  9900  fzctr  9903  flid  10050  flqeqceilz  10084  faclbnd3  10482  bcn1  10497  isfinite4im  10532  leabs  10839  gcd0id  11656  lcmgcdlem  11747  dvdsnprmd  11795  eltpsg  12196  tg1  12217  cldval  12257  cldss  12263  cldopn  12265  psmetdmdm  12482  dvef  12845  bj-nn0suc0  13137