Theorem mpancom 426

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpan  428  spesbc  3138  onsucelsucr  4655  sucunielr  4657  ordsuc  4710  peano2b  4762  xpiindim  4917  fununfun  5424  fvelrnb  5750  fliftcnv  6001  riotaprop  6064  unielxp  6408  dmtpos  6527  tpossym  6547  ercnv  6828  cnvct  7097  php5dom  7164  3xpfi  7241  recrecnq  7761  1idpr  7959  eqlei2  8420  lem1  9177  eluzfz1  10435  fzpred  10477  uznfz  10510  fz0fzdiffz0  10537  fzctr  10540  flid  10719  flqeqceilz  10755  faclbnd3  11181  bcn1  11196  isfinite4im  11231  hashfac  11288  leabs  11840  gcd0id  12756  lcmgcdlem  12855  dvdsnprmd  12903  pcprod  13125  fldivp1  13127  intopsn  13687  mgm1  13690  sgrp1  13726  mnd1  13762  mnd1id  13763  grp1  13911  grp1inv  13912  eqger  14027  eqgid  14029  qusghm  14085  rngressid  14253  ring1  14364  ringressid  14368  subrgsubm  14542  resrhm2b  14557  lssex  14691  cncrng  14906  ressascl  15039  psrbagfsupp  15055  psrbaglesupp  15058  eltpsg  15141  tg1  15160  cldval  15200  cldss  15206  cldopn  15208  psmetdmdm  15425  dvef  15828  relogef  15965  zabsle1  16118  usgredg2vlem2  16464  wlkprop  16568  wlkvtxiedg  16586  eupthseg  16693  bj-nn0suc0  16976