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

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
mpancom.2
Assertion
Ref Expression
mpancom

Proof of Theorem mpancom
StepHypRef Expression
1 mpancom.1 . 2
2 id 22 . 2
3 mpancom.2 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  mpan  670  spesbc  3420  xpiindi  5143  fununfun  5637  dffv2  5946  fliftcnv  6209  riotaprop  6281  elovmpt3rab1  6536  3xpexg  6603  orduniorsuc  6665  unielxp  6836  dmtpos  6986  tpossym  7006  oesuclem  7194  ercnv  7351  undom  7625  sucxpdom  7749  3xpfi  7812  pwfilem  7834  rankr1id  8301  cardnn  8365  alephnbtwn2  8474  alephsucdom  8481  cdainflem  8592  isfin4-3  8716  axcclem  8858  infxpidm  8958  fpwwe2lem9  9037  gchpwdom  9069  elwina  9085  elina  9086  rankcf  9176  ltexprlem4  9438  lem1  10408  ltdivp1i  10497  rpnnen1lem5  11241  eluzfz1  11722  fzpred  11757  uznfz  11790  fz0fzdiffz0  11812  fzctr  11816  flid  11945  modid0  12021  2txmodxeq0  12047  faclbnd3  12370  faclbnd4lem4  12374  bcn1  12391  hashfac  12507  hash2prv  12525  hash2sspr  12526  repswsymballbi  12752  wrdlen2i  12884  sqrtsq  13103  absrdbnd  13174  sqreulem  13192  sqreu  13193  gcd0id  14161  pcprod  14414  fldivp1  14416  invsym2  15157  pleval2i  15594  subrgsubm  17442  cncrng  18439  znchr  18601  mattposvs  18957  smadiadetglem2  19174  tg1  19465  cldval  19524  cldss  19530  cldopn  19532  1stcrestlem  19953  refbas  20011  refssex  20012  regr1  20251  kqreg  20252  kqnrm  20253  ufilen  20431  symgtgp  20600  elrnust  20727  psmetdmdm  20809  metuvalOLD  21052  metuval  21053  icoopnst  21439  cnheiborlem  21454  cfilfcls  21713  eflogeq  22986  logdivlt  23006  logdifbnd  23323  harmonicbnd4  23340  basellem5  23358  bposlem7  23565  chto1ub  23661  chpo1ub  23665  vmadivsum  23667  dchrmusum2  23679  dchrvmasum2if  23682  dchrvmasumlema  23685  dchrvmasumiflem2  23687  dchrisum0re  23698  dchrvmasumlem  23708  rplogsum  23712  mulogsumlem  23716  logdivsum  23718  selberg2lem  23735  pntrmax  23749  pntlem3  23794  pntleml  23796  pnt2  23798  usgraidx2vlem2  24392  nbcusgra  24463  uvtxnbgravtx  24495  cusgrauvtxb  24496  wlkbprop  24523  wlkonprop  24535  trlonprop  24544  pthonprop  24579  spthonprp  24587  usgra2adedgspthlem1  24611  usgra2adedgwlk  24614  cyclispthon  24633  fargshiftfva  24639  constr3lem4  24647  constr3trllem2  24651  4cycl4dv  24667  wlklniswwlkn1  24699  clwlkiswlk  24757  clwwlkf  24794  wwlkext2clwwlk  24803  erclwwlknsym  24826  erclwwlkntr  24827  clwlkfclwwlk  24844  eupatrl  24968  frgra1v  24998  frgrancvvdeqlem3  25032  numclwlk1lem2fo  25095  numclwlk2lem2f  25103  numclwwlk5lem  25111  issubgoi  25312  ismgmOLD  25322  ismndo2  25347  ablomul  25357  rngomndo  25423  vcoprnelem  25471  hilablo  26077  mayete3i  26646  mayete3iOLD  26647  homulid2  26719  adjeu  26808  lnopeqi  26927  cnlnadjlem7  26992  adjbdlnb  27003  nmopcoadji  27020  bracnlnval  27033  elunirn2  27489  dmct  27537  cnvct  27538  mptct  27541  mptctf  27544  xraddge02  27577  xrge0npcan  27684  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  metidval  27869  pstmval  27874  baselsiga  28115  sigasspw  28116  ddeval1  28206  ddeval0  28207  braew  28214  derangen2  28618  subfaclim  28632  snmlff  28774  elfzm12  29041  relexp0  29052  relexpsucr  29053  relexp1  29054  relexpcnv  29056  relexpadd  29061  relexpindlem  29062  dfrtrclrec2  29066  rtrclreclem.trans  29069  rtrclreclem.min  29070  bpoly2  29819  wl-sbal1  30013  ismblfin  30055  itg2addnclem2  30067  areacirclem2  30108  areacirc  30112  fnetr  30169  prter3  30623  mzpsubmpt  30675  mzpnegmpt  30676  lcmgcdlem  31212  afveu  32238  usgra2pthspth  32351  lindsrng01  33069  uunT1  33577  atbase  35014  llnbase  35233  lplnbase  35258  lvolbase  35302  lhpbase  35722
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
  Copyright terms: Public domain W3C validator