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  6119  xpexr  7909  bropopvvv  8076  bropfvvvv  8078  reldmtpos  8219  zeo  12648  rpneg  13006  xrlttri  13118  difreicc  13461  pfxnd0  14638  nn0o1gt2  16324  cshwshashlem1  17029  gsumcom3fi  19847  gsumbagdiagOLD  21492  psrass1lemOLD  21493  gsumbagdiag  21495  psrass1lem  21496  cfinufil  23432  2sq2  26936  2sqnn0  26941  sltlpss  27402  sizusglecusg  28751  iswspthsnon  29141  clwlkclwwlklem2a4  29281  frgrncvvdeqlem8  29590  chirredi  31678  gsummpt2co  32231  truae  33272  bj-sngltag  35912  itg2addnclem  36587  itg2addnclem3  36589  cdleme32e  39364  dflim5  42127  ntrneiiso  42890  tz6.12-afv  45929  tz6.12-afv2  45996  odz2prm2pw  46279  lighneallem3  46323  lighneallem4b  46325  lindslinindsimp2lem5  47191  nnolog2flm1  47324  2itscp  47515