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  6119  xpexr  7909  bropopvvv  8076  bropfvvvv  8078  reldmtpos  8219  zeo  12648  rpneg  13006  xrlttri  13118  difreicc  13461  pfxnd0  14638  nn0o1gt2  16324  cshwshashlem1  17029  gsumcom3fi  19847  gsumbagdiagOLD  21492  psrass1lemOLD  21493  gsumbagdiag  21495  psrass1lem  21496  cfinufil  23432  2sq2  26936  2sqnn0  26941  sltlpss  27401  sizusglecusg  28720  iswspthsnon  29110  clwlkclwwlklem2a4  29250  frgrncvvdeqlem8  29559  chirredi  31647  gsummpt2co  32200  truae  33241  bj-sngltag  35864  itg2addnclem  36539  itg2addnclem3  36541  cdleme32e  39316  dflim5  42079  ntrneiiso  42842  tz6.12-afv  45881  tz6.12-afv2  45948  odz2prm2pw  46231  lighneallem3  46275  lighneallem4b  46277  lindslinindsimp2lem5  47143  nnolog2flm1  47276  2itscp  47467