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  6061  xpexr  7843  bropopvvv  8015  bropfvvvv  8017  reldmtpos  8159  zeo  12551  rpneg  12916  xrlttri  13030  difreicc  13376  pfxnd0  14588  nn0o1gt2  16284  cshwshashlem1  16999  gsumcom3fi  19884  gsumbagdiag  21861  psrass1lem  21862  cfinufil  23836  2sq2  27364  2sqnn0  27369  sltlpss  27846  sizusglecusg  29435  iswspthsnon  29827  clwlkclwwlklem2a4  29967  frgrncvvdeqlem8  30276  chirredi  32364  gsummpt2co  33018  truae  34246  bj-sngltag  36996  itg2addnclem  37690  itg2addnclem3  37692  cdleme32e  40463  dflim5  43341  ntrneiiso  44103  tz6.12-afv  47183  tz6.12-afv2  47250  odz2prm2pw  47573  lighneallem3  47617  lighneallem4b  47619  lindslinindsimp2lem5  48473  nnolog2flm1  48601  2itscp  48792  oppcmndclem  49028