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  839  asymref2  6104  xpexr  7899  bropopvvv  8069  bropfvvvv  8071  reldmtpos  8214  zeo  12669  rpneg  13037  xrlttri  13151  difreicc  13498  pfxnd0  14712  nn0o1gt2  16425  cshwshashlem1  17141  gsumcom3fi  20029  gsumbagdiag  21991  psrass1lem  21992  cfinufil  23995  2sq2  27504  2sqnn0  27509  ltslpss  28008  sizusglecusg  29671  iswspthsnon  30063  clwlkclwwlklem2a4  30206  frgrncvvdeqlem8  30515  chirredi  32604  gsummpt2co  33234  truae  34542  bj-sngltag  37473  itg2addnclem  38175  itg2addnclem3  38177  cdleme32e  41074  dflim5  43911  ntrneiiso  44672  tz6.12-afv  47758  tz6.12-afv2  47825  odz2prm2pw  48163  lighneallem3  48207  lighneallem4b  48209  lindslinindsimp2lem5  49075  nnolog2flm1  49203  2itscp  49394  oppcmndclem  49629