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  837  asymref2  6090  xpexr  7884  bropopvvv  8053  bropfvvvv  8055  reldmtpos  8198  zeo  12645  rpneg  13013  xrlttri  13127  difreicc  13474  pfxnd0  14688  nn0o1gt2  16387  cshwshashlem1  17103  gsumcom3fi  19991  gsumbagdiag  21953  psrass1lem  21954  cfinufil  23957  2sq2  27463  2sqnn0  27468  ltslpss  27967  sizusglecusg  29599  iswspthsnon  29991  clwlkclwwlklem2a4  30134  frgrncvvdeqlem8  30443  chirredi  32532  gsummpt2co  33178  truae  34484  bj-sngltag  37406  itg2addnclem  38108  itg2addnclem3  38110  cdleme32e  41007  dflim5  43844  ntrneiiso  44605  tz6.12-afv  47705  tz6.12-afv2  47772  odz2prm2pw  48110  lighneallem3  48154  lighneallem4b  48156  lindslinindsimp2lem5  49022  nnolog2flm1  49150  2itscp  49341  oppcmndclem  49576