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  827  asymref2  6123  xpexr  7924  bropopvvv  8093  bropfvvvv  8095  reldmtpos  8238  zeo  12678  rpneg  13038  xrlttri  13150  difreicc  13493  pfxnd0  14670  nn0o1gt2  16357  cshwshashlem1  17064  gsumcom3fi  19938  gsumbagdiagOLD  21877  psrass1lemOLD  21878  gsumbagdiag  21880  psrass1lem  21881  cfinufil  23862  2sq2  27396  2sqnn0  27401  sltlpss  27863  sizusglecusg  29333  iswspthsnon  29723  clwlkclwwlklem2a4  29863  frgrncvvdeqlem8  30172  chirredi  32260  gsummpt2co  32819  truae  33932  bj-sngltag  36532  itg2addnclem  37214  itg2addnclem3  37216  cdleme32e  39987  dflim5  42823  ntrneiiso  43586  tz6.12-afv  46616  tz6.12-afv2  46683  odz2prm2pw  46966  lighneallem3  47010  lighneallem4b  47012  lindslinindsimp2lem5  47642  nnolog2flm1  47775  2itscp  47966