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  2540  2mo  2550  mosubopt  4937  predpoirr  5672  predfrirr  5673  funfv  6227  dffv2  6233  fvmptnf  6263  rdgsucmptnf  7477  frsucmptn  7486  mapdom2  8082  frfi  8156  oiexg  8391  wemapwe  8545  r1tr  8590  alephsing  9049  uzin  11671  fundmge2nop0  13220  fun2dmnop0  13222  sumrblem  14382  fsumcvg  14383  summolem2a  14386  fsumcvg2  14398  prodeq2ii  14575  prodrblem  14591  fprodcvg  14592  prodmolem2a  14596  zprod  14599  ptpjpre1  21293  qtopres  21420  fgabs  21602  ptcmplem3  21777  setsmstopn  22202  tngtopn  22373  cnmpt2pc  22646  pcoval2  22735  pcopt  22741  pcopt2  22742  itgle  23495  ibladdlem  23505  iblabslem  23513  iblabs  23514  iblabsr  23515  iblmulc2  23516  ditgneg  23540  umgr2adedgspth  26726  n4cyclfrgr  27032  poimirlem26  33094  poimirlem32  33100  ovoliunnfl  33110  voliunnfl  33112  volsupnfl  33113  itg2addnclem  33120  itg2gt0cn  33124  ibladdnclem  33125  iblabsnclem  33132  iblabsnc  33133  iblmulc2nc  33134  bddiblnc  33139  ftc1anclem7  33150  ftc1anclem8  33151  ftc1anc  33152  dicvalrelN  35981  dihvalrel  36075  ldepspr  41571
 Copyright terms: Public domain W3C validator