Theorem mpancom 669

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

Syntax hints:   -> wi 4   /\ wa 369

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 371

This theorem is referenced by:  mpan  670  spesbc  3284  xpiindi  4980  fununfun  5467  dffv2  5769  fliftcnv  6009  riotaprop  6081  orduniorsuc  6446  unielxp  6617  dmtpos  6762  tpossym  6782  oesuclem  6970  ercnv  7127  undom  7404  sucxpdom  7527  pwfilem  7610  rankr1id  8074  cardnn  8138  alephnbtwn2  8247  alephsucdom  8254  cdainflem  8365  isfin4-3  8489  axcclem  8631  infxpidm  8731  fpwwe2lem9  8810  gchpwdom  8842  elwina  8858  elina  8859  rankcf  8949  ltexprlem4  9213  lem1  10175  ltdivp1i  10264  rpnnen1lem5  10988  eluzfz1  11463  fz0fzdiffz0  11494  fzpred  11508  fzctr  11534  uznfz  11548  flid  11662  modid0  11738  2txmodxeq0  11764  faclbnd3  12073  faclbnd4lem4  12077  bcn1  12094  hashfac  12216  repswsymballbi  12423  wrdlen2i  12551  sqrsq  12764  absrdbnd  12834  sqreulem  12852  sqreu  12853  gcd0id  13712  pcprod  13962  fldivp1  13964  invsym2  14706  pleval2i  15139  subrgsubm  16883  cncrng  17842  znchr  18000  mattposvs  18344  smadiadetglem2  18483  tg1  18574  cldval  18632  cldss  18638  cldopn  18640  1stcrestlem  19061  regr1  19328  kqreg  19329  kqnrm  19330  ufilen  19508  symgtgp  19677  elrnust  19804  psmetdmdm  19886  metuvalOLD  20129  metuval  20130  icoopnst  20516  cnheiborlem  20531  cfilfcls  20790  eflogeq  22055  logdivlt  22075  logdifbnd  22392  harmonicbnd4  22409  basellem5  22427  bposlem7  22634  chto1ub  22730  chpo1ub  22734  vmadivsum  22736  dchrmusum2  22748  dchrvmasum2if  22751  dchrvmasumlema  22754  dchrvmasumiflem2  22756  dchrisum0re  22767  dchrvmasumlem  22777  rplogsum  22781  mulogsumlem  22785  logdivsum  22787  selberg2lem  22804  pntrmax  22818  pntlem3  22863  pntleml  22865  pnt2  22867  usgraidx2vlem2  23315  nbcusgra  23376  uvtxnbgravtx  23408  cusgrauvtxb  23409  wlkonprop  23436  wlkbprop  23438  trlonprop  23446  pthonprop  23481  spthonprp  23489  cyclispthon  23524  fargshiftfva  23530  constr3lem4  23538  constr3trllem2  23542  4cycl4dv  23558  eupatrl  23594  issubgoi  23802  ismgm  23812  ismndo2  23837  ablomul  23847  rngomndo  23913  vcoprnelem  23961  hilablo  24567  mayete3i  25136  mayete3iOLD  25137  homulid2  25209  adjeu  25298  lnopeqi  25417  cnlnadjlem7  25482  adjbdlnb  25493  nmopcoadji  25510  bracnlnval  25523  elunirn2  25971  dmct  26019  cnvct  26020  mptct  26023  mptctf  26026  xraddge02  26055  xrge0npcan  26162  gsumle  26251  gsumvsca1  26256  gsumvsca2  26257  metidval  26322  pstmval  26327  baselsiga  26563  sigasspw  26564  ddeval1  26655  ddeval0  26656  braew  26663  derangen2  27067  subfaclim  27081  snmlff  27223  elfzm12  27325  relexp0  27336  relexpsucr  27337  relexp1  27338  relexpcnv  27340  relexpadd  27345  relexpindlem  27346  dfrtrclrec2  27350  rtrclreclem.trans  27353  rtrclreclem.min  27354  bpoly2  28205  ismblfin  28437  itg2addnclem2  28449  areacirclem2  28490  areacirc  28494  refbas  28557  refssex  28558  fnetr  28563  prter3  29032  mzpsubmpt  29084  mzpnegmpt  29085  afveu  30064  3xpexg  30125  elovmpt3rab1  30168  3xpfi  30171  hash2prv  30231  hash2sspr  30232  ccats1rev  30265  usgra2pthspth  30300  usgra2adedgspthlem1  30308  usgra2adedgwlk  30311  wlklniswwlkn1  30338  2wlkonot  30389  2spthonot  30390  2spotfi  30416  clwlkiswlk  30427  clwwlkf  30461  wwlkext2clwwlk  30470  erclwwlknsym  30505  erclwwlkntr  30506  clwlkfclwwlk  30522  frgra1v  30595  frgrancvvdeqlem3  30630  2spotmdisj  30666  numclwlk1lem2fo  30693  numclwlk2lem2f  30701  numclwwlk5lem  30709  lindsrng01  31007  uunT1  31518  atbase  32939  llnbase  33158  lplnbase  33183  lvolbase  33227  lhpbase  33647