Theorem mpancom 673

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  mpan  674  spesbc  3387  xpiindi  4990  fununfun  5645  dffv2  5954  fliftcnv  6219  riotaprop  6290  elovmpt3rab1  6541  3xpexg  6608  orduniorsuc  6671  unielxp  6843  dmtpos  6993  tpossym  7013  oesuclem  7235  ercnv  7392  undom  7666  sucxpdom  7787  3xpfi  7849  pwfilem  7874  rankr1id  8332  cardnn  8396  alephnbtwn2  8501  alephsucdom  8508  cdainflem  8619  isfin4-3  8743  axcclem  8885  infxpidm  8985  fpwwe2lem9  9062  gchpwdom  9094  elwina  9110  elina  9111  rankcf  9201  ltexprlem4  9463  lem1  10445  ltdivp1i  10533  rpnnen1lem5  11294  eluzfz1  11804  fzpred  11842  uznfz  11875  fz0fzdiffz0  11897  fzctr  11901  flid  12041  modid0  12119  2txmodxeq0  12147  faclbnd3  12474  faclbnd4lem4  12478  bcn1  12495  hashfac  12616  hash2prv  12634  hash2sspr  12635  repswsymballbi  12868  wrdlen2i  13000  dfrtrclrec2  13099  rtrclreclem3  13102  rtrclreclem4  13103  relexpindlem  13105  sqrtsq  13312  absrdbnd  13383  sqreulem  13401  sqreu  13402  bpoly2  14088  gcd0id  14461  lcmgcdlem  14542  lcmftp  14580  pcprod  14803  fldivp1  14805  invsym2  15619  pleval2i  16161  subrgsubm  17956  cncrng  18924  znchr  19064  mattposvs  19411  smadiadetglem2  19628  tg1  19910  cldval  19969  cldss  19975  cldopn  19977  1stcrestlem  20398  refbas  20456  refssex  20457  regr1  20696  kqreg  20697  kqnrm  20698  ufilen  20876  symgtgp  21047  elrnust  21170  psmetdmdm  21252  metuval  21495  icoopnst  21863  cnheiborlem  21878  cfilfcls  22137  eflogeq  23416  logdivlt  23435  logdifbnd  23784  harmonicbnd4  23801  basellem5  23874  bposlem7  24081  chto1ub  24177  chpo1ub  24181  vmadivsum  24183  dchrmusum2  24195  dchrvmasum2if  24198  dchrvmasumlema  24201  dchrvmasumiflem2  24203  dchrisum0re  24214  dchrvmasumlem  24224  rplogsum  24228  mulogsumlem  24232  logdivsum  24234  selberg2lem  24251  pntrmax  24265  pntlem3  24310  pntleml  24312  pnt2  24314  usgraidx2vlem2  24965  nbcusgra  25036  uvtxnbgravtx  25068  cusgrauvtxb  25069  wlkbprop  25096  wlkonprop  25108  trlonprop  25117  pthonprop  25152  spthonprp  25160  usgra2adedgspthlem1  25184  usgra2adedgwlk  25187  cyclispthon  25206  fargshiftfva  25212  constr3lem4  25220  constr3trllem2  25224  4cycl4dv  25240  wlklniswwlkn1  25272  clwlkiswlk  25330  clwwlkf  25367  wwlkext2clwwlk  25376  erclwwlknsym  25399  erclwwlkntr  25400  clwlkfclwwlk  25417  eupatrl  25541  frgra1v  25571  frgrancvvdeqlem3  25605  numclwlk1lem2fo  25668  numclwlk2lem2f  25676  numclwwlk5lem  25684  issubgoi  25883  ismgmOLD  25893  ismndo2  25918  ablomul  25928  rngomndo  25994  vcoprnelem  26042  hilablo  26648  mayete3i  27216  homulid2  27288  adjeu  27377  lnopeqi  27496  cnlnadjlem7  27561  adjbdlnb  27572  nmopcoadji  27589  bracnlnval  27602  elunirn2  28090  dmct  28141  cnvct  28142  mptct  28145  mptctf  28148  xraddge02  28177  xrge0npcan  28295  gsumle  28380  gsumvsca1  28384  gsumvsca2  28385  metidval  28532  pstmval  28537  baselsiga  28776  sigasspw  28777  ddeval1  28896  ddeval0  28897  braew  28904  derangen2  29685  subfaclim  29699  snmlff  29840  elfzm12  30107  fnetr  30792  wl-sbal1  31600  poimirlem13  31657  poimirlem14  31658  poimirlem31  31675  poimirlem32  31676  ismblfin  31685  itg2addnclem2  31698  areacirclem2  31737  areacirc  31741  prter3  32162  atbase  32564  llnbase  32783  lplnbase  32808  lvolbase  32852  lhpbase  33272  mzpsubmpt  35294  mzpnegmpt  35295  eliunov2  35910  iunrelexp0  35933  uunT1  36807  nnfoctb  37023  afveu  38045  fzopredsuc  38110  usgra2pthspth  38421  lindsrng01  39021