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

Theorem pm2.24d 151
Description: Deduction form of pm2.24 124. (Contributed by NM, 30-Jan-2006.)
Hypothesis
Ref Expression
pm2.24d.1 (𝜑𝜓)
Assertion
Ref Expression
pm2.24d (𝜑 → (¬ 𝜓𝜒))

Proof of Theorem pm2.24d
StepHypRef Expression
1 pm2.24d.1 . . 3 (𝜑𝜓)
21a1d 25 . 2 (𝜑 → (¬ 𝜒𝜓))
32con1d 145 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.5g  168  impimprbi  828  asymref2  6076  xpexr  7860  bropopvvv  8027  bropfvvvv  8029  reldmtpos  8170  zeo  12596  rpneg  12954  xrlttri  13065  difreicc  13408  pfxnd0  14583  nn0o1gt2  16270  cshwshashlem1  16975  gsumcom3fi  19763  gsumbagdiagOLD  21357  psrass1lemOLD  21358  gsumbagdiag  21360  psrass1lem  21361  cfinufil  23295  2sq2  26797  2sqnn0  26802  sltlpss  27258  sizusglecusg  28453  iswspthsnon  28843  clwlkclwwlklem2a4  28983  frgrncvvdeqlem8  29292  chirredi  31378  gsummpt2co  31932  truae  32882  bj-sngltag  35483  itg2addnclem  36158  itg2addnclem3  36160  cdleme32e  38937  dflim5  41693  ntrneiiso  42437  tz6.12-afv  45479  tz6.12-afv2  45546  odz2prm2pw  45829  lighneallem3  45873  lighneallem4b  45875  lindslinindsimp2lem5  46617  nnolog2flm1  46750  2itscp  46941
  Copyright terms: Public domain W3C validator