Theorem pm2.24d 152

Description: Deduction form of pm2.24 125. (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 26	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3	2	con1d 146	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  169  impimprbi  841  asymref2  6117  xpexr  7914  bropopvvv  8084  bropfvvvv  8086  reldmtpos  8229  zeo  12681  rpneg  13049  xrlttri  13163  difreicc  13510  pfxnd0  14725  nn0o1gt2  16438  cshwshashlem1  17154  gsumcom3fi  20048  gsumbagdiag  22061  psrass1lem  22062  cfinufil  24064  2sq2  27573  2sqnn0  27578  ltslpss  28077  sizusglecusg  29779  iswspthsnon  30171  clwlkclwwlklem2a4  30314  frgrncvvdeqlem8  30623  chirredi  32712  gsummpt2co  33334  truae  34599  bj-sngltag  37585  itg2addnclem  38288  itg2addnclem3  38290  cdleme32e  41187  dflim5  44026  ntrneiiso  44787  tz6.12-afv  47877  tz6.12-afv2  47944  odz2prm2pw  48282  lighneallem3  48326  lighneallem4b  48328  lindslinindsimp2lem5  49209  nnolog2flm1  49337  2itscp  49528  oppcmndclem  49762