Theorem mpancom 419

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 409	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  421  spesbc  2998  onsucelsucr  4432  sucunielr  4434  ordsuc  4486  peano2b  4536  xpiindim  4684  fvelrnb  5477  fliftcnv  5704  riotaprop  5761  unielxp  6080  dmtpos  6161  tpossym  6181  ercnv  6458  cnvct  6711  php5dom  6765  3xpfi  6827  recrecnq  7226  1idpr  7424  eqlei2  7882  lem1  8629  eluzfz1  9842  fzpred  9881  uznfz  9914  fz0fzdiffz0  9938  fzctr  9941  flid  10088  flqeqceilz  10122  faclbnd3  10521  bcn1  10536  isfinite4im  10571  leabs  10878  gcd0id  11703  lcmgcdlem  11794  dvdsnprmd  11842  eltpsg  12246  tg1  12267  cldval  12307  cldss  12313  cldopn  12315  psmetdmdm  12532  dvef  12896  relogef  12993  bj-nn0suc0  13319