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  829  asymref2  6081  xpexr  7869  bropopvvv  8040  bropfvvvv  8042  reldmtpos  8184  zeo  12615  rpneg  12976  xrlttri  13090  difreicc  13437  pfxnd0  14651  nn0o1gt2  16350  cshwshashlem1  17066  gsumcom3fi  19954  gsumbagdiag  21911  psrass1lem  21912  cfinufil  23893  2sq2  27396  2sqnn0  27401  ltslpss  27900  sizusglecusg  29532  iswspthsnon  29924  clwlkclwwlklem2a4  30067  frgrncvvdeqlem8  30376  chirredi  32465  gsummpt2co  33109  truae  34387  bj-sngltag  37290  itg2addnclem  37992  itg2addnclem3  37994  cdleme32e  40891  dflim5  43757  ntrneiiso  44518  tz6.12-afv  47615  tz6.12-afv2  47682  odz2prm2pw  48020  lighneallem3  48064  lighneallem4b  48066  lindslinindsimp2lem5  48932  nnolog2flm1  49060  2itscp  49251  oppcmndclem  49486