Theorem mpancom 420

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  422  spesbc  3040  onsucelsucr  4490  sucunielr  4492  ordsuc  4545  peano2b  4597  xpiindim  4746  fvelrnb  5542  fliftcnv  5771  riotaprop  5829  unielxp  6150  dmtpos  6232  tpossym  6252  ercnv  6530  cnvct  6783  php5dom  6837  3xpfi  6904  recrecnq  7343  1idpr  7541  eqlei2  8001  lem1  8750  eluzfz1  9974  fzpred  10013  uznfz  10046  fz0fzdiffz0  10073  fzctr  10076  flid  10227  flqeqceilz  10261  faclbnd3  10664  bcn1  10679  isfinite4im  10714  leabs  11025  gcd0id  11921  lcmgcdlem  12018  dvdsnprmd  12066  pcprod  12285  fldivp1  12287  intopsn  12607  mgm1  12610  sgrp1  12637  mnd1  12665  mnd1id  12666  eltpsg  12753  tg1  12774  cldval  12814  cldss  12820  cldopn  12822  psmetdmdm  13039  dvef  13403  relogef  13500  zabsle1  13615  bj-nn0suc0  13907