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 149
Description: Deduction form of pm2.24 122. (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 142 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.5  166  asymref2  5729  xpexr  7339  bropopvvv  7490  bropfvvvv  7492  reldmtpos  7596  zeo  11749  rpneg  12104  xrlttri  12215  difreicc  12554  pfxnd0  13728  nn0o1gt2  15430  cshwshashlem1  16127  gsumbagdiag  19696  psrass1lem  19697  gsumcom3fi  20528  cfinufil  22057  sizusglecusg  26705  iswspthsnon  27101  clwlkclwwlklem2a4  27282  frgrncvvdeqlem8  27647  chirredi  29770  gsummpt2co  30288  truae  30814  bj-sngltag  33455  itg2addnclem  33941  itg2addnclem3  33943  cdleme32e  36458  ntrneiiso  39159  tz6.12-afv  42015  tz6.12-afv2  42082  odz2prm2pw  42245  lighneallem3  42294  lighneallem4b  42296  lindslinindsimp2lem5  43038  nnolog2flm1  43171
  Copyright terms: Public domain W3C validator