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  6090  xpexr  7894  bropopvvv  8069  bropfvvvv  8071  reldmtpos  8213  zeo  12620  rpneg  12985  xrlttri  13099  difreicc  13445  pfxnd0  14653  nn0o1gt2  16351  cshwshashlem1  17066  gsumcom3fi  19909  gsumbagdiag  21840  psrass1lem  21841  cfinufil  23815  2sq2  27344  2sqnn0  27349  sltlpss  27819  sizusglecusg  29391  iswspthsnon  29786  clwlkclwwlklem2a4  29926  frgrncvvdeqlem8  30235  chirredi  32323  gsummpt2co  32988  truae  34233  bj-sngltag  36971  itg2addnclem  37665  itg2addnclem3  37667  cdleme32e  40439  dflim5  43318  ntrneiiso  44080  tz6.12-afv  47174  tz6.12-afv2  47241  odz2prm2pw  47564  lighneallem3  47608  lighneallem4b  47610  lindslinindsimp2lem5  48451  nnolog2flm1  48579  2itscp  48770  oppcmndclem  49006