Theorem pm2.24d 154

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 147	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  170  impimprbi  826  asymref2  5977  xpexr  7623  bropopvvv  7785  bropfvvvv  7787  reldmtpos  7900  zeo  12069  rpneg  12422  xrlttri  12533  difreicc  12871  pfxnd0  14050  nn0o1gt2  15732  cshwshashlem1  16429  gsumcom3fi  19099  gsumbagdiag  20156  psrass1lem  20157  cfinufil  22536  2sq2  26009  2sqnn0  26014  sizusglecusg  27245  iswspthsnon  27634  clwlkclwwlklem2a4  27775  frgrncvvdeqlem8  28085  chirredi  30171  gsummpt2co  30686  truae  31502  bj-sngltag  34298  itg2addnclem  34958  itg2addnclem3  34960  cdleme32e  37596  ntrneiiso  40490  tz6.12-afv  43421  tz6.12-afv2  43488  odz2prm2pw  43774  lighneallem3  43821  lighneallem4b  43823  lindslinindsimp2lem5  44566  nnolog2flm1  44699  2itscp  44817