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  6140  xpexr  7941  bropopvvv  8114  bropfvvvv  8116  reldmtpos  8258  zeo  12702  rpneg  13065  xrlttri  13178  difreicc  13521  pfxnd0  14723  nn0o1gt2  16415  cshwshashlem1  17130  gsumcom3fi  20012  gsumbagdiag  21969  psrass1lem  21970  cfinufil  23952  2sq2  27492  2sqnn0  27497  sltlpss  27960  sizusglecusg  29496  iswspthsnon  29886  clwlkclwwlklem2a4  30026  frgrncvvdeqlem8  30335  chirredi  32423  gsummpt2co  33034  truae  34224  bj-sngltag  36966  itg2addnclem  37658  itg2addnclem3  37660  cdleme32e  40428  dflim5  43319  ntrneiiso  44081  tz6.12-afv  47123  tz6.12-afv2  47190  odz2prm2pw  47488  lighneallem3  47532  lighneallem4b  47534  lindslinindsimp2lem5  48308  nnolog2flm1  48440  2itscp  48631