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 154
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 147 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  169  impimprbi  826  asymref2  5975  xpexr  7611  bropopvvv  7776  bropfvvvv  7778  reldmtpos  7891  zeo  12057  rpneg  12411  xrlttri  12522  difreicc  12860  pfxnd0  14040  nn0o1gt2  15722  cshwshashlem1  16419  gsumcom3fi  19019  gsumbagdiag  20075  psrass1lem  20076  cfinufil  22452  2sq2  25923  2sqnn0  25928  sizusglecusg  27159  iswspthsnon  27548  clwlkclwwlklem2a4  27689  frgrncvvdeqlem8  27999  chirredi  30085  gsummpt2co  30600  truae  31388  bj-sngltag  34179  itg2addnclem  34810  itg2addnclem3  34812  cdleme32e  37448  ntrneiiso  40306  tz6.12-afv  43238  tz6.12-afv2  43305  odz2prm2pw  43557  lighneallem3  43604  lighneallem4b  43606  lindslinindsimp2lem5  44349  nnolog2flm1  44482  2itscp  44600
  Copyright terms: Public domain W3C validator