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

Theorem mpancom 654
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 21 . 2
3 mpancom.2 . 2
41, 2, 3syl2anc 646 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362
This theorem is referenced by:  mpan  655  spesbc  3256  xpiindi  4946  dffv2  5734  fliftcnv  5972  riotaprop  6045  orduniorsuc  6411  unielxp  6581  dmtpos  6719  tpossym  6739  oesuclem  6926  ercnv  7083  undom  7358  sucxpdom  7481  pwfilem  7564  rabfsupp  7606  rankr1id  8016  cardnn  8080  alephnbtwn2  8189  alephsucdom  8196  cdainflem  8307  isfin4-3  8431  axcclem  8573  infxpidm  8673  fpwwe2lem9  8751  gchpwdom  8783  elwina  8799  elina  8800  rankcf  8890  ltexprlem4  9154  lem1  10116  ltdivp1i  10205  rpnnen1lem5  10928  eluzfz1  11402  fz0fzdiffz0  11433  fzctr  11470  uznfz  11484  flid  11598  modid0  11674  2txmodxeq0  11700  faclbnd3  12009  faclbnd4lem4  12013  bcn1  12030  hashfac  12152  repswsymballbi  12359  wrdlen2i  12487  sqrsq  12700  absrdbnd  12770  sqreulem  12788  sqreu  12789  gcd0id  13647  pcprod  13897  fldivp1  13899  invsym2  14641  pleval2i  15074  subrgsubm  16691  cncrng  17547  znchr  17703  mattposvs  18037  smadiadetglem2  18182  tg1  18273  cldval  18331  cldss  18337  cldopn  18339  1stcrestlem  18760  regr1  19027  kqreg  19028  kqnrm  19029  ufilen  19207  symgtgp  19376  elrnust  19499  psmetdmdm  19581  metuvalOLD  19824  metuval  19825  icoopnst  20211  cnheiborlem  20226  cfilfcls  20485  eflogeq  21791  logdivlt  21811  logdifbnd  22128  harmonicbnd4  22145  basellem5  22163  bposlem7  22370  chto1ub  22466  chpo1ub  22470  vmadivsum  22472  dchrmusum2  22484  dchrvmasum2if  22487  dchrvmasumlema  22490  dchrvmasumiflem2  22492  dchrisum0re  22503  dchrvmasumlem  22513  rplogsum  22517  mulogsumlem  22521  logdivsum  22523  selberg2lem  22540  pntrmax  22554  pntlem3  22599  pntleml  22601  pnt2  22603  usgraidx2vlem2  22989  nbcusgra  23050  uvtxnbgravtx  23082  cusgrauvtxb  23083  wlkonprop  23110  wlkbprop  23112  trlonprop  23120  pthonprop  23155  spthonprp  23163  cyclispthon  23198  fargshiftfva  23204  constr3lem4  23212  constr3trllem2  23216  4cycl4dv  23232  eupatrl  23268  issubgoi  23476  ismgm  23486  ismndo2  23511  ablomul  23521  rngomndo  23587  vcoprnelem  23635  hilablo  24241  mayete3i  24810  mayete3iOLD  24811  homulid2  24883  adjeu  24972  lnopeqi  25091  cnlnadjlem7  25156  adjbdlnb  25167  nmopcoadji  25184  bracnlnval  25197  elunirn2  25646  dmct  25694  cnvct  25695  mptct  25698  mptctf  25701  xraddge02  25730  xrge0npcan  25836  gsumle  25953  gsumvsca1  25959  gsumvsca2  25960  metidval  26026  pstmval  26031  baselsiga  26267  sigasspw  26268  ddeval1  26359  ddeval0  26360  braew  26367  derangen2  26765  subfaclim  26779  snmlff  26921  elfzm12  27022  relexp0  27033  relexpsucr  27034  relexp1  27035  relexpcnv  27037  relexpadd  27042  relexpindlem  27043  dfrtrclrec2  27047  rtrclreclem.trans  27050  rtrclreclem.min  27051  bpoly2  27902  ismblfin  28103  itg2addnclem2  28115  areacirclem2  28156  areacirc  28160  refbas  28223  refssex  28224  fnetr  28229  prter3  28699  mzpsubmpt  28752  mzpnegmpt  28753  afveu  29733  3xpexg  29794  elovmpt3rab1  29837  3xpfi  29840  hash2prv  29900  hash2sspr  29901  ccats1rev  29934  usgra2pthspth  29969  usgra2adedgspthlem1  29977  usgra2adedgwlk  29980  wlklniswwlkn1  30007  2wlkonot  30058  2spthonot  30059  2spotfi  30085  clwlkiswlk  30096  clwwlkf  30130  wwlkext2clwwlk  30139  erclwwlknsym  30174  erclwwlkntr  30175  clwlkfclwwlk  30191  frgra1v  30264  frgrancvvdeqlem3  30299  2spotmdisj  30335  numclwlk1lem2fo  30362  numclwlk2lem2f  30370  numclwwlk5lem  30378  lindsrng01  30586  uunT1  31091  atbase  32371  llnbase  32590  lplnbase  32615  lvolbase  32659  lhpbase  33079
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 179  df-an 364
  Copyright terms: Public domain W3C validator