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  5548  xpexr  7148  bropopvvv  7300  bropfvvvv  7302  reldmtpos  7405  zeo  11501  rpneg  11901  xrlttri  12010  difreicc  12342  nn0o1gt2  15144  cshwshashlem1  15849  gsumbagdiag  19424  psrass1lem  19425  gsumcom3fi  20254  cfinufil  21779  sizusglecusg  26415  iswspthsnon  26806  clwlkclwwlklem2a4  26963  frgrncvvdeqlem8  27286  chirredi  29381  gsummpt2co  29908  truae  30434  bj-sngltag  33096  itg2addnclem  33591  itg2addnclem3  33593  cdleme32e  36050  ntrneiiso  38706  tz6.12-afv  41574  odz2prm2pw  41800  lighneallem3  41849  lighneallem4b  41851  lindslinindsimp2lem5  42576  nnolog2flm1  42709