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

Step	Hyp	Ref	Expression
1		pm2.24d.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3	2	con1d 142	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.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