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  5954  xpexr  7634  bropopvvv  7796  bropfvvvv  7798  reldmtpos  7916  zeo  12120  rpneg  12475  xrlttri  12586  difreicc  12929  pfxnd0  14110  nn0o1gt2  15795  cshwshashlem1  16501  gsumcom3fi  19181  gsumbagdiagOLD  20715  psrass1lemOLD  20716  gsumbagdiag  20718  psrass1lem  20719  cfinufil  22642  2sq2  26130  2sqnn0  26135  sizusglecusg  27366  iswspthsnon  27755  clwlkclwwlklem2a4  27895  frgrncvvdeqlem8  28204  chirredi  30290  gsummpt2co  30847  truae  31743  bj-sngltag  34735  itg2addnclem  35423  itg2addnclem3  35425  cdleme32e  38056  ntrneiiso  41212  tz6.12-afv  44156  tz6.12-afv2  44223  odz2prm2pw  44507  lighneallem3  44551  lighneallem4b  44553  lindslinindsimp2lem5  45295  nnolog2flm1  45428  2itscp  45619