MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpancom Structured version   Unicode version

Theorem mpancom 664
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
StepHypRef Expression
1 mpancom.1 . 2  |-  ( ps 
->  ph )
2 id 22 . 2  |-  ( ps 
->  ps )
3 mpancom.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 656 1  |-  ( ps 
->  ch )
Colors of variables: wff setvar class
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  665  spesbc  3276  xpiindi  4971  fununfun  5459  dffv2  5761  fliftcnv  6001  riotaprop  6074  orduniorsuc  6440  unielxp  6611  dmtpos  6756  tpossym  6776  oesuclem  6961  ercnv  7118  undom  7395  sucxpdom  7518  pwfilem  7601  rankr1id  8065  cardnn  8129  alephnbtwn2  8238  alephsucdom  8245  cdainflem  8356  isfin4-3  8480  axcclem  8622  infxpidm  8722  fpwwe2lem9  8801  gchpwdom  8833  elwina  8849  elina  8850  rankcf  8940  ltexprlem4  9204  lem1  10166  ltdivp1i  10255  rpnnen1lem5  10979  eluzfz1  11454  fz0fzdiffz0  11485  fzpred  11499  fzctr  11525  uznfz  11539  flid  11653  modid0  11729  2txmodxeq0  11755  faclbnd3  12064  faclbnd4lem4  12068  bcn1  12085  hashfac  12207  repswsymballbi  12414  wrdlen2i  12542  sqrsq  12755  absrdbnd  12825  sqreulem  12843  sqreu  12844  gcd0id  13703  pcprod  13953  fldivp1  13955  invsym2  14697  pleval2i  15130  subrgsubm  16858  cncrng  17796  znchr  17954  mattposvs  18298  smadiadetglem2  18437  tg1  18528  cldval  18586  cldss  18592  cldopn  18594  1stcrestlem  19015  regr1  19282  kqreg  19283  kqnrm  19284  ufilen  19462  symgtgp  19631  elrnust  19758  psmetdmdm  19840  metuvalOLD  20083  metuval  20084  icoopnst  20470  cnheiborlem  20485  cfilfcls  20744  eflogeq  22009  logdivlt  22029  logdifbnd  22346  harmonicbnd4  22363  basellem5  22381  bposlem7  22588  chto1ub  22684  chpo1ub  22688  vmadivsum  22690  dchrmusum2  22702  dchrvmasum2if  22705  dchrvmasumlema  22708  dchrvmasumiflem2  22710  dchrisum0re  22721  dchrvmasumlem  22731  rplogsum  22735  mulogsumlem  22739  logdivsum  22741  selberg2lem  22758  pntrmax  22772  pntlem3  22817  pntleml  22819  pnt2  22821  usgraidx2vlem2  23245  nbcusgra  23306  uvtxnbgravtx  23338  cusgrauvtxb  23339  wlkonprop  23366  wlkbprop  23368  trlonprop  23376  pthonprop  23411  spthonprp  23419  cyclispthon  23454  fargshiftfva  23460  constr3lem4  23468  constr3trllem2  23472  4cycl4dv  23488  eupatrl  23524  issubgoi  23732  ismgm  23742  ismndo2  23767  ablomul  23777  rngomndo  23843  vcoprnelem  23891  hilablo  24497  mayete3i  25066  mayete3iOLD  25067  homulid2  25139  adjeu  25228  lnopeqi  25347  cnlnadjlem7  25412  adjbdlnb  25423  nmopcoadji  25440  bracnlnval  25453  elunirn2  25901  dmct  25949  cnvct  25950  mptct  25953  mptctf  25956  xraddge02  25985  xrge0npcan  26090  gsumle  26181  gsumvsca1  26186  gsumvsca2  26187  metidval  26253  pstmval  26258  baselsiga  26494  sigasspw  26495  ddeval1  26586  ddeval0  26587  braew  26594  derangen2  26992  subfaclim  27006  snmlff  27148  elfzm12  27249  relexp0  27260  relexpsucr  27261  relexp1  27262  relexpcnv  27264  relexpadd  27269  relexpindlem  27270  dfrtrclrec2  27274  rtrclreclem.trans  27277  rtrclreclem.min  27278  bpoly2  28129  ismblfin  28357  itg2addnclem2  28369  areacirclem2  28410  areacirc  28414  refbas  28477  refssex  28478  fnetr  28483  prter3  28952  mzpsubmpt  29004  mzpnegmpt  29005  afveu  29984  3xpexg  30045  elovmpt3rab1  30088  3xpfi  30091  hash2prv  30151  hash2sspr  30152  ccats1rev  30185  usgra2pthspth  30220  usgra2adedgspthlem1  30228  usgra2adedgwlk  30231  wlklniswwlkn1  30258  2wlkonot  30309  2spthonot  30310  2spotfi  30336  clwlkiswlk  30347  clwwlkf  30381  wwlkext2clwwlk  30390  erclwwlknsym  30425  erclwwlkntr  30426  clwlkfclwwlk  30442  frgra1v  30515  frgrancvvdeqlem3  30550  2spotmdisj  30586  numclwlk1lem2fo  30613  numclwlk2lem2f  30621  numclwwlk5lem  30629  lindsrng01  30843  uunT1  31347  atbase  32656  llnbase  32875  lplnbase  32900  lvolbase  32944  lhpbase  33364
  Copyright terms: Public domain W3C validator