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  6069  xpexr  7858  bropopvvv  8029  bropfvvvv  8031  reldmtpos  8173  zeo  12604  rpneg  12965  xrlttri  13079  difreicc  13426  pfxnd0  14640  nn0o1gt2  16339  cshwshashlem1  17055  gsumcom3fi  19943  gsumbagdiag  21900  psrass1lem  21901  cfinufil  23881  2sq2  27384  2sqnn0  27389  ltslpss  27888  sizusglecusg  29520  iswspthsnon  29912  clwlkclwwlklem2a4  30055  frgrncvvdeqlem8  30364  chirredi  32453  gsummpt2co  33097  truae  34375  bj-sngltag  37278  itg2addnclem  37980  itg2addnclem3  37982  cdleme32e  40879  dflim5  43745  ntrneiiso  44506  tz6.12-afv  47609  tz6.12-afv2  47676  odz2prm2pw  48014  lighneallem3  48058  lighneallem4b  48060  lindslinindsimp2lem5  48926  nnolog2flm1  49054  2itscp  49245  oppcmndclem  49480