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  825  asymref2  6011  xpexr  7739  bropopvvv  7901  bropfvvvv  7903  reldmtpos  8021  zeo  12336  rpneg  12691  xrlttri  12802  difreicc  13145  pfxnd0  14329  nn0o1gt2  16018  cshwshashlem1  16725  gsumcom3fi  19495  gsumbagdiagOLD  21052  psrass1lemOLD  21053  gsumbagdiag  21055  psrass1lem  21056  cfinufil  22987  2sq2  26486  2sqnn0  26491  sizusglecusg  27733  iswspthsnon  28122  clwlkclwwlklem2a4  28262  frgrncvvdeqlem8  28571  chirredi  30657  gsummpt2co  31210  truae  32111  sltlpss  34014  bj-sngltag  35100  itg2addnclem  35755  itg2addnclem3  35757  cdleme32e  38386  ntrneiiso  41590  tz6.12-afv  44552  tz6.12-afv2  44619  odz2prm2pw  44903  lighneallem3  44947  lighneallem4b  44949  lindslinindsimp2lem5  45691  nnolog2flm1  45824  2itscp  46015