Theorem mpancom 667

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

Syntax hints:   -> wi 4   /\ wa 367

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 185  df-an 369

This theorem is referenced by:  mpan  668  spesbc  3406  xpiindi  5127  fununfun  5614  dffv2  5921  fliftcnv  6184  riotaprop  6255  elovmpt3rab1  6509  3xpexg  6576  orduniorsuc  6638  unielxp  6809  dmtpos  6959  tpossym  6979  oesuclem  7167  ercnv  7324  undom  7598  sucxpdom  7722  3xpfi  7784  pwfilem  7806  rankr1id  8271  cardnn  8335  alephnbtwn2  8444  alephsucdom  8451  cdainflem  8562  isfin4-3  8686  axcclem  8828  infxpidm  8928  fpwwe2lem9  9005  gchpwdom  9037  elwina  9053  elina  9054  rankcf  9144  ltexprlem4  9406  lem1  10379  ltdivp1i  10467  rpnnen1lem5  11213  eluzfz1  11696  fzpred  11732  uznfz  11765  fz0fzdiffz0  11787  fzctr  11791  flid  11926  modid0  12004  2txmodxeq0  12032  faclbnd3  12355  faclbnd4lem4  12359  bcn1  12376  hashfac  12494  hash2prv  12512  hash2sspr  12513  repswsymballbi  12746  wrdlen2i  12878  dfrtrclrec2  12975  rtrclreclem3  12978  rtrclreclem4  12979  relexpindlem  12981  sqrtsq  13188  absrdbnd  13259  sqreulem  13277  sqreu  13278  gcd0id  14248  pcprod  14501  fldivp1  14503  invsym2  15254  pleval2i  15796  subrgsubm  17640  cncrng  18637  znchr  18777  mattposvs  19127  smadiadetglem2  19344  tg1  19635  cldval  19694  cldss  19700  cldopn  19702  1stcrestlem  20122  refbas  20180  refssex  20181  regr1  20420  kqreg  20421  kqnrm  20422  ufilen  20600  symgtgp  20769  elrnust  20896  psmetdmdm  20978  metuvalOLD  21221  metuval  21222  icoopnst  21608  cnheiborlem  21623  cfilfcls  21882  eflogeq  23158  logdivlt  23177  logdifbnd  23524  harmonicbnd4  23541  basellem5  23559  bposlem7  23766  chto1ub  23862  chpo1ub  23866  vmadivsum  23868  dchrmusum2  23880  dchrvmasum2if  23883  dchrvmasumlema  23886  dchrvmasumiflem2  23888  dchrisum0re  23899  dchrvmasumlem  23909  rplogsum  23913  mulogsumlem  23917  logdivsum  23919  selberg2lem  23936  pntrmax  23950  pntlem3  23995  pntleml  23997  pnt2  23999  usgraidx2vlem2  24597  nbcusgra  24668  uvtxnbgravtx  24700  cusgrauvtxb  24701  wlkbprop  24728  wlkonprop  24740  trlonprop  24749  pthonprop  24784  spthonprp  24792  usgra2adedgspthlem1  24816  usgra2adedgwlk  24819  cyclispthon  24838  fargshiftfva  24844  constr3lem4  24852  constr3trllem2  24856  4cycl4dv  24872  wlklniswwlkn1  24904  clwlkiswlk  24962  clwwlkf  24999  wwlkext2clwwlk  25008  erclwwlknsym  25031  erclwwlkntr  25032  clwlkfclwwlk  25049  eupatrl  25173  frgra1v  25203  frgrancvvdeqlem3  25237  numclwlk1lem2fo  25300  numclwlk2lem2f  25308  numclwwlk5lem  25316  issubgoi  25513  ismgmOLD  25523  ismndo2  25548  ablomul  25558  rngomndo  25624  vcoprnelem  25672  hilablo  26278  mayete3i  26847  mayete3iOLD  26848  homulid2  26920  adjeu  27009  lnopeqi  27128  cnlnadjlem7  27193  adjbdlnb  27204  nmopcoadji  27221  bracnlnval  27234  elunirn2  27713  dmct  27770  cnvct  27771  mptct  27774  mptctf  27777  xraddge02  27811  xrge0npcan  27921  gsumle  28007  gsumvsca1  28011  gsumvsca2  28012  metidval  28107  pstmval  28112  baselsiga  28348  sigasspw  28349  ddeval1  28446  ddeval0  28447  braew  28454  derangen2  28885  subfaclim  28899  snmlff  29041  elfzm12  29308  bpoly2  30050  wl-sbal1  30256  ismblfin  30298  itg2addnclem2  30310  areacirclem2  30351  areacirc  30355  fnetr  30412  prter3  30866  mzpsubmpt  30918  mzpnegmpt  30919  lcmgcdlem  31456  afveu  32480  usgra2pthspth  32742  lindsrng01  33342  uunT1  33990  atbase  35430  llnbase  35649  lplnbase  35674  lvolbase  35718  lhpbase  36138  eliunov2  38221  iunrelexp0  38245