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  6117  xpexr  7920  bropopvvv  8089  bropfvvvv  8091  reldmtpos  8233  zeo  12670  rpneg  13030  xrlttri  13142  difreicc  13485  pfxnd0  14662  nn0o1gt2  16349  cshwshashlem1  17056  gsumcom3fi  19925  gsumbagdiagOLD  21860  psrass1lemOLD  21861  gsumbagdiag  21863  psrass1lem  21864  cfinufil  23819  2sq2  27353  2sqnn0  27358  sltlpss  27820  sizusglecusg  29264  iswspthsnon  29654  clwlkclwwlklem2a4  29794  frgrncvvdeqlem8  30103  chirredi  32191  gsummpt2co  32740  truae  33798  bj-sngltag  36398  itg2addnclem  37079  itg2addnclem3  37081  cdleme32e  39855  dflim5  42681  ntrneiiso  43444  tz6.12-afv  46476  tz6.12-afv2  46543  odz2prm2pw  46826  lighneallem3  46870  lighneallem4b  46872  lindslinindsimp2lem5  47453  nnolog2flm1  47586  2itscp  47777