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

Theorem pm2.61d1 171
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 170 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  ja  173  pm2.61nii  178  pm2.01d  181  moexex  2570  2mo  2580  mosubopt  5001  predpoirr  5746  predfrirr  5747  funfv  6304  dffv2  6310  fvmptnf  6341  rdgsucmptnf  7570  frsucmptn  7579  mapdom2  8172  frfi  8246  oiexg  8481  wemapwe  8632  r1tr  8677  alephsing  9136  uzin  11758  fundmge2nop0  13312  fun2dmnop0  13314  sumrblem  14486  fsumcvg  14487  summolem2a  14490  fsumcvg2  14502  prodeq2ii  14687  prodrblem  14703  fprodcvg  14704  prodmolem2a  14708  zprod  14711  ptpjpre1  21422  qtopres  21549  fgabs  21730  ptcmplem3  21905  setsmstopn  22330  tngtopn  22501  cnmpt2pc  22774  pcoval2  22862  pcopt  22868  pcopt2  22869  itgle  23621  ibladdlem  23631  iblabslem  23639  iblabs  23640  iblabsr  23641  iblmulc2  23642  ditgneg  23666  umgr2adedgspth  26913  n4cyclfrgr  27271  poimirlem26  33565  poimirlem32  33571  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  itg2addnclem  33591  itg2gt0cn  33595  ibladdnclem  33596  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  bddiblnc  33610  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  dicvalrelN  36791  dihvalrel  36885  ldepspr  42587
  Copyright terms: Public domain W3C validator