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

Theorem pm2.24d 147
 Description: Deduction form of pm2.24 121. (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 139 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  164  asymref2  5663  xpexr  7263  bropopvvv  7415  bropfvvvv  7417  reldmtpos  7521  zeo  11647  rpneg  12048  xrlttri  12157  difreicc  12489  nn0o1gt2  15291  cshwshashlem1  15996  gsumbagdiag  19570  psrass1lem  19571  gsumcom3fi  20400  cfinufil  21925  sizusglecusg  26561  iswspthsnon  26953  clwlkclwwlklem2a4  27112  frgrncvvdeqlem8  27452  chirredi  29554  gsummpt2co  30081  truae  30607  bj-sngltag  33269  itg2addnclem  33766  itg2addnclem3  33768  cdleme32e  36227  ntrneiiso  38883  tz6.12-afv  41751  odz2prm2pw  41977  lighneallem3  42026  lighneallem4b  42028  lindslinindsimp2lem5  42753  nnolog2flm1  42886
 Copyright terms: Public domain W3C validator