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  6149  xpexr  7958  bropopvvv  8131  bropfvvvv  8133  reldmtpos  8275  zeo  12729  rpneg  13089  xrlttri  13201  difreicc  13544  pfxnd0  14736  nn0o1gt2  16429  cshwshashlem1  17143  gsumcom3fi  20021  gsumbagdiag  21974  psrass1lem  21975  cfinufil  23957  2sq2  27495  2sqnn0  27500  sltlpss  27963  sizusglecusg  29499  iswspthsnon  29889  clwlkclwwlklem2a4  30029  frgrncvvdeqlem8  30338  chirredi  32426  gsummpt2co  33031  truae  34207  bj-sngltag  36949  itg2addnclem  37631  itg2addnclem3  37633  cdleme32e  40402  dflim5  43291  ntrneiiso  44053  tz6.12-afv  47088  tz6.12-afv2  47155  odz2prm2pw  47437  lighneallem3  47481  lighneallem4b  47483  lindslinindsimp2lem5  48191  nnolog2flm1  48324  2itscp  48515