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

Step	Hyp	Ref	Expression
1		pm2.24d.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3	2	con1d 147	1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))

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  171  impimprbi  827  asymref2  5944  xpexr  7605  bropopvvv  7768  bropfvvvv  7770  reldmtpos  7883  zeo  12056  rpneg  12409  xrlttri  12520  difreicc  12862  pfxnd0  14041  nn0o1gt2  15722  cshwshashlem1  16421  gsumcom3fi  19092  gsumbagdiag  20614  psrass1lem  20615  cfinufil  22533  2sq2  26017  2sqnn0  26022  sizusglecusg  27253  iswspthsnon  27642  clwlkclwwlklem2a4  27782  frgrncvvdeqlem8  28091  chirredi  30177  gsummpt2co  30733  truae  31612  bj-sngltag  34419  itg2addnclem  35108  itg2addnclem3  35110  cdleme32e  37741  ntrneiiso  40794  tz6.12-afv  43729  tz6.12-afv2  43796  odz2prm2pw  44080  lighneallem3  44125  lighneallem4b  44127  lindslinindsimp2lem5  44871  nnolog2flm1  45004  2itscp  45195