Theorem mpancom 414

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 404	1 |- ( ps -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpan  416  spesbc  2927  onsucelsucr  4340  sucunielr  4342  ordsuc  4394  peano2b  4444  xpiindim  4588  fvelrnb  5367  fliftcnv  5590  riotaprop  5647  unielxp  5960  dmtpos  6037  tpossym  6057  ercnv  6329  cnvct  6582  php5dom  6635  3xpfi  6697  recrecnq  7016  1idpr  7214  eqlei2  7642  lem1  8371  eluzfz1  9508  fzpred  9547  uznfz  9580  fz0fzdiffz0  9604  fzctr  9607  flid  9754  flqeqceilz  9788  faclbnd3  10214  bcn1  10229  isfinite4im  10264  leabs  10570  gcd0id  11311  lcmgcdlem  11400  dvdsnprmd  11448  eltpsg  11801  tg1  11822  cldval  11862  cldss  11868  cldopn  11870  bj-nn0suc0  12149