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  3424  xpiindi  5136  fununfun  5630  dffv2  5938  fliftcnv  6195  riotaprop  6267  elovmpt3rab1  6518  orduniorsuc  6643  3xpexg  6710  unielxp  6817  dmtpos  6964  tpossym  6984  oesuclem  7172  ercnv  7329  undom  7602  sucxpdom  7726  3xpfi  7788  pwfilem  7810  rankr1id  8276  cardnn  8340  alephnbtwn2  8449  alephsucdom  8456  cdainflem  8567  isfin4-3  8691  axcclem  8833  infxpidm  8933  fpwwe2lem9  9012  gchpwdom  9044  elwina  9060  elina  9061  rankcf  9151  ltexprlem4  9413  lem1  10379  ltdivp1i  10468  rpnnen1lem5  11208  eluzfz1  11689  fzpred  11724  uznfz  11757  fz0fzdiffz0  11777  fzctr  11780  flid  11909  modid0  11985  2txmodxeq0  12011  faclbnd3  12334  faclbnd4lem4  12338  bcn1  12355  hashfac  12469  hash2prv  12487  hash2sspr  12488  repswsymballbi  12711  wrdlen2i  12843  sqrtsq  13062  absrdbnd  13133  sqreulem  13151  sqreu  13152  gcd0id  14016  pcprod  14269  fldivp1  14271  invsym2  15014  pleval2i  15447  subrgsubm  17225  cncrng  18210  znchr  18368  mattposvs  18724  smadiadetglem2  18941  tg1  19232  cldval  19290  cldss  19296  cldopn  19298  1stcrestlem  19719  regr1  19986  kqreg  19987  kqnrm  19988  ufilen  20166  symgtgp  20335  elrnust  20462  psmetdmdm  20544  metuvalOLD  20787  metuval  20788  icoopnst  21174  cnheiborlem  21189  cfilfcls  21448  eflogeq  22714  logdivlt  22734  logdifbnd  23051  harmonicbnd4  23068  basellem5  23086  bposlem7  23293  chto1ub  23389  chpo1ub  23393  vmadivsum  23395  dchrmusum2  23407  dchrvmasum2if  23410  dchrvmasumlema  23413  dchrvmasumiflem2  23415  dchrisum0re  23426  dchrvmasumlem  23436  rplogsum  23440  mulogsumlem  23444  logdivsum  23446  selberg2lem  23463  pntrmax  23477  pntlem3  23522  pntleml  23524  pnt2  23526  usgraidx2vlem2  24068  nbcusgra  24139  uvtxnbgravtx  24171  cusgrauvtxb  24172  wlkbprop  24199  wlkonprop  24211  trlonprop  24220  pthonprop  24255  spthonprp  24263  usgra2adedgspthlem1  24287  usgra2adedgwlk  24290  cyclispthon  24309  fargshiftfva  24315  constr3lem4  24323  constr3trllem2  24327  4cycl4dv  24343  wlklniswwlkn1  24375  clwlkiswlk  24433  clwwlkf  24470  wwlkext2clwwlk  24479  erclwwlknsym  24502  erclwwlkntr  24503  clwlkfclwwlk  24520  2wlkonot  24541  2spthonot  24542  2spotfi  24568  eupatrl  24644  frgra1v  24674  frgrancvvdeqlem3  24709  2spotmdisj  24745  numclwlk1lem2fo  24772  numclwlk2lem2f  24780  numclwwlk5lem  24788  issubgoi  24988  ismgm  24998  ismndo2  25023  ablomul  25033  rngomndo  25099  vcoprnelem  25147  hilablo  25753  mayete3i  26322  mayete3iOLD  26323  homulid2  26395  adjeu  26484  lnopeqi  26603  cnlnadjlem7  26668  adjbdlnb  26679  nmopcoadji  26696  bracnlnval  26709  elunirn2  27161  dmct  27209  cnvct  27210  mptct  27213  mptctf  27216  xraddge02  27245  xrge0npcan  27346  gsumle  27433  gsumvsca1  27436  gsumvsca2  27437  metidval  27505  pstmval  27510  baselsiga  27755  sigasspw  27756  ddeval1  27846  ddeval0  27847  braew  27854  derangen2  28258  subfaclim  28272  snmlff  28414  elfzm12  28516  relexp0  28527  relexpsucr  28528  relexp1  28529  relexpcnv  28531  relexpadd  28536  relexpindlem  28537  dfrtrclrec2  28541  rtrclreclem.trans  28544  rtrclreclem.min  28545  bpoly2  29396  ismblfin  29632  itg2addnclem2  29644  areacirclem2  29685  areacirc  29689  refbas  29752  refssex  29753  fnetr  29758  prter3  30227  mzpsubmpt  30279  mzpnegmpt  30280  lcmgcdlem  30812  afveu  31705  usgra2pthspth  31820  lindsrng01  32142  uunT1  32657  atbase  34086  llnbase  34305  lplnbase  34330  lvolbase  34374  lhpbase  34794