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  2626  2mo  2648  mosubopt  5465  predpoirr  6285  predfrirr  6286  funfv  6925  dffv2  6933  fvmptnf  6967  rdgsucmptnf  8371  frsucmptn  8381  mapdom2  9088  frfi  9228  oiexg  9467  wemapwe  9629  r1tr  9708  alephsing  10208  uzin  12795  fundmge2nop0  14383  fun2dmnop0  14385  wrdnfi  14428  relexpsucrd  14910  relexpsucld  14911  relexpreld  14917  relexpdmd  14921  relexprnd  14925  relexpfldd  14927  relexpaddd  14931  dfrtrclrec2  14935  rtrclreclem4  14938  dfrtrcl2  14939  relexpindlem  14940  sumrblem  15588  fsumcvg  15589  summolem2a  15592  fsumcvg2  15604  prodeq2ii  15788  prodrblem  15804  fprodcvg  15805  prodmolem2a  15809  zprod  15812  ptpjpre1  22906  qtopres  23033  fgabs  23214  ptcmplem3  23389  setsmstopn  23817  tngtopn  23998  cnmpopc  24275  pcoval2  24363  pcopt  24369  pcopt2  24370  itgle  25158  ibladdlem  25168  iblabslem  25176  iblabs  25177  iblabsr  25178  iblmulc2  25179  bddiblnc  25190  ditgneg  25205  logbgcd1irr  26128  umgr2adedgspth  28779  n4cyclfrgr  29121  poimirlem26  36071  poimirlem32  36077  ovoliunnfl  36087  voliunnfl  36089  volsupnfl  36090  itg2addnclem  36096  itg2gt0cn  36100  ibladdnclem  36101  iblabsnclem  36108  iblabsnc  36109  iblmulc2nc  36110  ftc1anclem7  36124  ftc1anclem8  36125  ftc1anc  36126  dicvalrelN  39615  dihvalrel  39709  ldepspr  46486  naryfval  46646  naryfvalixp  46647
  Copyright terms: Public domain W3C validator