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 180
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 179 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:  pm2.61nii  184  ja  186  pm2.01d  189  moexexlem  2627  2mo  2649  mosubopt  5465  predpoirr  6285  predfrirr  6286  funfv  6925  dffv2  6933  fvmptnf  6967  rdgsucmptnf  8367  frsucmptn  8377  mapdom2  9050  frfi  9190  oiexg  9429  wemapwe  9591  r1tr  9670  alephsing  10170  uzin  12757  fundmge2nop0  14345  fun2dmnop0  14347  wrdnfi  14390  relexpsucrd  14878  relexpsucld  14879  relexpreld  14885  relexpdmd  14889  relexprnd  14893  relexpfldd  14895  relexpaddd  14899  dfrtrclrec2  14903  rtrclreclem4  14906  dfrtrcl2  14907  relexpindlem  14908  sumrblem  15556  fsumcvg  15557  summolem2a  15560  fsumcvg2  15572  prodeq2ii  15756  prodrblem  15772  fprodcvg  15773  prodmolem2a  15777  zprod  15780  ptpjpre1  22874  qtopres  23001  fgabs  23182  ptcmplem3  23357  setsmstopn  23785  tngtopn  23966  cnmpopc  24243  pcoval2  24331  pcopt  24337  pcopt2  24338  itgle  25126  ibladdlem  25136  iblabslem  25144  iblabs  25145  iblabsr  25146  iblmulc2  25147  bddiblnc  25158  ditgneg  25173  logbgcd1irr  26096  umgr2adedgspth  28722  n4cyclfrgr  29064  poimirlem26  36042  poimirlem32  36048  ovoliunnfl  36058  voliunnfl  36060  volsupnfl  36061  itg2addnclem  36067  itg2gt0cn  36071  ibladdnclem  36072  iblabsnclem  36079  iblabsnc  36080  iblmulc2nc  36081  ftc1anclem7  36095  ftc1anclem8  36096  ftc1anc  36097  dicvalrelN  39586  dihvalrel  39680  ldepspr  46455  naryfval  46615  naryfvalixp  46616
  Copyright terms: Public domain W3C validator