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

Theorem pm2.61d1 159
Description: Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)
Hypotheses
Ref Expression
pm2.61d1.1
pm2.61d1.2
Assertion
Ref Expression
pm2.61d1

Proof of Theorem pm2.61d1
StepHypRef Expression
1 pm2.61d1.1 . 2
2 pm2.61d1.2 . . 3
32a1i 11 . 2
41, 3pm2.61d 158 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  ja  161  pm2.61nii  166  pm2.01d  169  moexex  2363  2mo  2373  2moOLD  2374  mosubopt  4750  funfv  5940  dffv2  5946  fvmptnf  5973  rdgsucmptnf  7114  frsucmptn  7123  mapdom2  7708  frfi  7785  oiexg  7981  wemapwe  8160  wemapweOLD  8161  r1tr  8215  alephsing  8677  uzin  11142  sumrblem  13533  fsumcvg  13534  summolem2a  13537  fsumcvg2  13549  prodeq2ii  13720  prodrblem  13736  fprodcvg  13737  prodmolem2a  13741  zprod  13744  ptpjpre1  20072  qtopres  20199  fgabs  20380  ptcmplem3  20554  setsmstopn  20981  tngtopn  21164  cnmpt2pc  21428  pcoval2  21516  pcopt  21522  pcopt2  21523  itgle  22216  ibladdlem  22226  iblabslem  22234  iblabs  22235  iblabsr  22236  iblmulc2  22237  ditgneg  22261  nbgra0nb  24429  n4cyclfrgra  25018  predpoirr  29277  predfrirr  29278  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  itg2addnclem  30066  itg2gt0cn  30070  ibladdnclem  30071  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  bddiblnc  30085  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  ldepspr  33074  dicvalrelN  36912  dihvalrel  37006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator