Theorem pm2.24d 151

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 145	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  168  impimprbi  828  asymref2  6117  xpexr  7920  bropopvvv  8089  bropfvvvv  8091  reldmtpos  8233  zeo  12672  rpneg  13032  xrlttri  13144  difreicc  13487  pfxnd0  14664  nn0o1gt2  16351  cshwshashlem1  17058  gsumcom3fi  19927  gsumbagdiagOLD  21866  psrass1lemOLD  21867  gsumbagdiag  21869  psrass1lem  21870  cfinufil  23825  2sq2  27359  2sqnn0  27364  sltlpss  27826  sizusglecusg  29270  iswspthsnon  29660  clwlkclwwlklem2a4  29800  frgrncvvdeqlem8  30109  chirredi  32197  gsummpt2co  32756  truae  33856  bj-sngltag  36456  itg2addnclem  37138  itg2addnclem3  37140  cdleme32e  39912  dflim5  42752  ntrneiiso  43515  tz6.12-afv  46547  tz6.12-afv2  46614  odz2prm2pw  46897  lighneallem3  46941  lighneallem4b  46943  lindslinindsimp2lem5  47524  nnolog2flm1  47657  2itscp  47848