Theorem pm2.24d 146

Description: Deduction form of pm2.24 120. (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 138	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  163  asymref2  5432  xpexr  6999  bropopvvv  7142  bropfvvvv  7144  reldmtpos  7247  zeo  11339  rpneg  11739  xrlttri  11848  difreicc  12175  nn0o1gt2  14935  cshwshashlem1  15640  gsumbagdiag  19197  psrass1lem  19198  gsumcom3fi  20025  cfinufil  21542  sizeusglecusg  26014  clwlkisclwwlklem2a4  26312  2wlkonot3v  26402  2spthonot3v  26403  frgrancvvdeqlemB  26565  chirredi  28637  gsummpt2co  29111  truae  29633  bj-sngltag  32164  itg2addnclem  32631  itg2addnclem3  32633  cdleme32e  34751  ntrneiiso  37409  tz6.12-afv  39902  odz2prm2pw  40013  lighneallem3  40062  lighneallem4b  40064  sizusglecusg  40679  clwlkclwwlklem2a4  41206  frgrncvvdeqlemB  41477  lindslinindsimp2lem5  42045  nnolog2flm1  42182