Theorem mpancom 680

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  mpan  681  spesbc  3361  xpiindi  4989  fununfun  5645  dffv2  5961  fliftcnv  6229  riotaprop  6300  elovmpt3rab1  6554  3xpexg  6621  orduniorsuc  6684  unielxp  6856  dmtpos  7011  tpossym  7031  oesuclem  7253  ercnv  7410  undom  7686  sucxpdom  7807  3xpfi  7869  pwfilem  7894  rankr1id  8359  cardnn  8423  alephnbtwn2  8529  alephsucdom  8536  cdainflem  8647  isfin4-3  8771  axcclem  8913  infxpidm  9013  fpwwe2lem9  9089  gchpwdom  9121  elwina  9137  elina  9138  rankcf  9228  ltexprlem4  9490  lem1  10474  ltdivp1i  10561  rpnnen1lem5  11323  eluzfz1  11835  fzpred  11873  uznfz  11906  fz0fzdiffz0  11929  fzctr  11933  flid  12076  modid0  12154  2txmodxeq0  12182  faclbnd3  12509  faclbnd4lem4  12513  bcn1  12530  hashfac  12654  repswsymballbi  12920  wrdlen2i  13067  dfrtrclrec2  13169  rtrclreclem3  13172  rtrclreclem4  13173  relexpindlem  13175  sqrtsq  13382  absrdbnd  13453  sqreulem  13471  sqreu  13472  bpoly2  14159  gcd0id  14536  lcmgcdlem  14620  lcmftp  14658  pcprod  14889  fldivp1  14891  invsym2  15717  pleval2i  16259  subrgsubm  18070  cncrng  19038  znchr  19182  mattposvs  19529  smadiadetglem2  19746  tg1  20028  cldval  20087  cldss  20093  cldopn  20095  1stcrestlem  20516  refbas  20574  refssex  20575  regr1  20814  kqreg  20815  kqnrm  20816  ufilen  20994  symgtgp  21165  elrnust  21288  psmetdmdm  21370  metuval  21613  icoopnst  22016  cnheiborlem  22031  cfilfcls  22293  eflogeq  23600  logdivlt  23619  logdifbnd  23968  harmonicbnd4  23985  basellem5  24060  bposlem7  24267  chto1ub  24363  chpo1ub  24367  vmadivsum  24369  dchrmusum2  24381  dchrvmasum2if  24384  dchrvmasumlema  24387  dchrvmasumiflem2  24389  dchrisum0re  24400  dchrvmasumlem  24410  rplogsum  24414  mulogsumlem  24418  logdivsum  24420  selberg2lem  24437  pntrmax  24451  pntlem3  24496  pntleml  24498  pnt2  24500  usgraidx2vlem2  25168  nbcusgra  25240  uvtxnbgravtx  25272  cusgrauvtxb  25273  wlkbprop  25300  wlkonprop  25312  trlonprop  25321  pthonprop  25356  spthonprp  25364  usgra2adedgspthlem1  25388  usgra2adedgwlk  25391  cyclispthon  25410  fargshiftfva  25416  constr3lem4  25424  constr3trllem2  25428  4cycl4dv  25444  wlklniswwlkn1  25476  clwlkiswlk  25534  clwwlkf  25571  wwlkext2clwwlk  25580  erclwwlknsym  25603  erclwwlkntr  25604  clwlkfclwwlk  25621  eupatrl  25745  frgra1v  25775  frgrancvvdeqlem3  25809  numclwlk1lem2fo  25872  numclwlk2lem2f  25880  numclwwlk5lem  25888  issubgoi  26087  ismgmOLD  26097  ismndo2  26122  ablomul  26132  rngomndo  26198  vcoprnelem  26246  hilablo  26862  mayete3i  27430  homulid2  27502  adjeu  27591  lnopeqi  27710  cnlnadjlem7  27775  adjbdlnb  27786  nmopcoadji  27803  bracnlnval  27816  elunirn2  28299  dmct  28347  cnvct  28348  mptct  28351  mptctf  28354  xraddge02  28385  xrge0npcan  28506  gsumle  28591  gsumvsca1  28594  gsumvsca2  28595  metidval  28742  pstmval  28747  baselsiga  28986  sigasspw  28987  ddeval1  29106  ddeval0  29107  braew  29114  derangen2  29946  subfaclim  29960  snmlff  30101  elfzm12  30368  fnetr  31056  wl-sbal1  31938  poimirlem13  31998  poimirlem14  31999  poimirlem31  32016  poimirlem32  32017  ismblfin  32026  itg2addnclem2  32039  areacirclem2  32078  areacirc  32082  prter3  32499  atbase  32900  llnbase  33119  lplnbase  33144  lvolbase  33188  lhpbase  33608  mzpsubmpt  35630  mzpnegmpt  35631  eliunov2  36316  iunrelexp0  36339  uunT1  37207  nnfoctb  37421  afveu  38693  fzopredsuc  38758  usgredg2vlem2  39353  1wlkop  39690  wlkOnprop  39709  1wlksonproplem  39740  usgra2pthspth  39938  lindsrng01  40534