Theorem mpancom 703

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 22	. 2 |- ( ps -> ps )
3		mpancom.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	1, 2, 3	syl2anc 693	1 |- ( ps -> ch )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mpan  706  spesbc  3521  xpiindi  5257  fununfun  5934  dffv2  6271  fliftcnv  6561  riotaprop  6635  elovmpt3rab1  6893  3xpexg  6961  orduniorsuc  7030  unielxp  7204  dmtpos  7364  tpossym  7384  oesuclem  7605  ercnv  7763  cnvct  8033  undom  8048  sucxpdom  8169  3xpfi  8232  pwfilem  8260  rankr1id  8725  cardnn  8789  alephnbtwn2  8895  alephsucdom  8902  cdainflem  9013  isfin4-3  9137  axcclem  9279  dmct  9346  mptct  9360  infxpidm  9384  fpwwe2lem9  9460  gchpwdom  9492  elwina  9508  elina  9509  rankcf  9599  ltexprlem4  9861  lem1  10864  ltdivp1i  10950  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  eluzfz1  12348  fzpred  12389  uznfz  12423  fz0fzdiffz0  12448  fzctr  12451  flid  12609  modid0  12696  2txmodxeq0  12730  faclbnd3  13079  faclbnd4lem4  13083  bcn1  13100  hashfac  13242  repswsymballbi  13527  wrdlen2i  13686  dfrtrclrec2  13797  rtrclreclem3  13800  rtrclreclem4  13801  relexpindlem  13803  sqrtsq  14010  absrdbnd  14081  sqreulem  14099  sqreu  14100  bpoly2  14788  gcd0id  15240  lcmgcdlem  15319  lcmftp  15349  dvdsnprmd  15403  pcprod  15599  fldivp1  15601  invsym2  16423  pleval2i  16964  subrgsubm  18793  cncrng  19767  znchr  19911  mattposvs  20261  smadiadetglem2  20478  tg1  20768  cldval  20827  cldss  20833  cldopn  20835  1stcrestlem  21255  refbas  21313  refssex  21314  regr1  21553  kqreg  21554  kqnrm  21555  ufilen  21734  symgtgp  21905  elrnust  22028  psmetdmdm  22110  metuval  22354  icoopnst  22738  cnheiborlem  22753  cfilfcls  23072  eflogeq  24348  logdivlt  24367  logdifbnd  24720  harmonicbnd4  24737  basellem5  24811  bposlem7  25015  zabsle1  25021  chto1ub  25165  chpo1ub  25169  vmadivsum  25171  dchrmusum2  25183  dchrvmasum2if  25186  dchrvmasumlema  25189  dchrvmasumiflem2  25191  dchrisum0re  25202  dchrvmasumlem  25212  rplogsum  25216  mulogsumlem  25220  logdivsum  25222  selberg2lem  25239  pntrmax  25253  pntlem3  25298  pntleml  25300  pnt2  25302  usgredg2vlem2  26118  vtxdgelxnn0  26368  wlkonprop  26554  wksonproplem  26601  wwlknbp  26733  wspthnp  26737  wlklnwwlkln1  26754  clwwlknbp0  26884  clwwlksf  26915  wwlksext2clwwlk  26924  erclwwlksnsym  26947  erclwwlksntr  26948  clwlksfclwwlk  26962  eupth0  27074  numclwlk1lem2fo  27228  numclwlk2lem2f  27236  numclwwlk5lem  27245  hilablo  28017  hhssabloilem  28118  mayete3i  28587  homulid2  28659  adjeu  28748  lnopeqi  28867  cnlnadjlem7  28932  adjbdlnb  28943  nmopcoadji  28960  bracnlnval  28973  elunirn2  29451  mptctf  29495  xraddge02  29521  xrge0npcan  29694  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  metidval  29933  pstmval  29938  baselsiga  30178  sigasspw  30179  ddeval1  30297  ddeval0  30298  braew  30305  derangen2  31156  subfaclim  31170  snmlff  31311  elfzm12  31569  noextendlt  31822  fnetr  32346  wl-sbal1  33346  poimirlem13  33422  poimirlem14  33423  poimirlem31  33440  poimirlem32  33441  ismblfin  33450  itg2addnclem2  33462  areacirclem2  33501  areacirc  33505  ismgmOLD  33649  ismndo2  33673  rngomndo  33734  prter3  34167  atbase  34576  llnbase  34795  lplnbase  34820  lvolbase  34864  lhpbase  35284  mzpsubmpt  37306  mzpnegmpt  37307  eliunov2  37971  iunrelexp0  37994  enmappwid  38294  uunT1  39007  nnfoctb  39213  afveu  41233  fzopredsuc  41333  fargshiftfva  41379  lindsrng01  42257