Theorem pm2.24d 147

Description: Deduction form of pm2.24 121. (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 139	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.5  164  asymref2  5513  xpexr  7106  bropopvvv  7255  bropfvvvv  7257  reldmtpos  7360  zeo  11463  rpneg  11863  xrlttri  11972  difreicc  12304  nn0o1gt2  15097  cshwshashlem1  15802  gsumbagdiag  19376  psrass1lem  19377  gsumcom3fi  20206  cfinufil  21732  sizusglecusg  26359  clwlkclwwlklem2a4  26898  frgrncvvdeqlem8  27170  chirredi  29253  gsummpt2co  29780  truae  30306  bj-sngltag  32971  itg2addnclem  33461  itg2addnclem3  33463  cdleme32e  35733  ntrneiiso  38389  tz6.12-afv  41253  odz2prm2pw  41475  lighneallem3  41524  lighneallem4b  41526  lindslinindsimp2lem5  42251  nnolog2flm1  42384