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  6072  xpexr  7860  bropopvvv  8031  bropfvvvv  8033  reldmtpos  8175  zeo  12579  rpneg  12940  xrlttri  13054  difreicc  13401  pfxnd0  14613  nn0o1gt2  16309  cshwshashlem1  17024  gsumcom3fi  19912  gsumbagdiag  21888  psrass1lem  21889  cfinufil  23871  2sq2  27384  2sqnn0  27389  ltslpss  27888  sizusglecusg  29521  iswspthsnon  29913  clwlkclwwlklem2a4  30056  frgrncvvdeqlem8  30365  chirredi  32454  gsummpt2co  33114  truae  34393  bj-sngltag  37288  itg2addnclem  37983  itg2addnclem3  37985  cdleme32e  40882  dflim5  43760  ntrneiiso  44521  tz6.12-afv  47607  tz6.12-afv2  47674  odz2prm2pw  47997  lighneallem3  48041  lighneallem4b  48043  lindslinindsimp2lem5  48896  nnolog2flm1  49024  2itscp  49215  oppcmndclem  49450