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  8421  lem1  9179  eluzfz1  10445  fzpred  10487  uznfz  10520  fz0fzdiffz0  10547  fzctr  10550  flid  10732  flqeqceilz  10768  faclbnd3  11195  bcn1  11210  isfinite4im  11245  hashfac  11302  leabs  11854  gcd0id  12772  lcmgcdlem  12871  dvdsnprmd  12919  pcprod  13145  fldivp1  13147  intopsn  13736  mgm1  13739  sgrp1  13775  mnd1  13811  mnd1id  13812  grp1  13960  grp1inv  13961  eqger  14076  eqgid  14078  qusghm  14134  rngressid  14302  ring1  14413  ringressid  14417  subrgsubm  14591  resrhm2b  14606  lssex  14740  cncrng  14955  ressascl  15088  psrbagfsupp  15104  psrbaglesupp  15107  eltpsg  15190  tg1  15209  cldval  15249  cldss  15255  cldopn  15257  psmetdmdm  15474  dvef  15877  relogef  16015  zabsle1  16216  usgredg2vlem2  16562  wlkprop  16666  wlkvtxiedg  16684  eupthseg  16791  bj-nn0suc0  17074