Theorem pm2.24d 152

Description: Deduction form of pm2.24 125. (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 26	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3	2	con1d 146	1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.5g  169  impimprbi  841  asymref2  6116  xpexr  7913  bropopvvv  8083  bropfvvvv  8085  reldmtpos  8228  zeo  12688  rpneg  13056  xrlttri  13170  difreicc  13517  pfxnd0  14733  nn0o1gt2  16445  cshwshashlem1  17161  gsumcom3fi  20055  gsumbagdiag  22093  psrass1lem  22094  cfinufil  24096  2sq2  27608  2sqnn0  27613  ltslpss  28112  sizusglecusg  29824  iswspthsnon  30216  clwlkclwwlklem2a4  30359  frgrncvvdeqlem8  30668  chirredi  32757  gsummpt2co  33377  truae  34642  bj-sngltag  37647  itg2addnclem  38350  itg2addnclem3  38352  cdleme32e  41247  dflim5  44084  ntrneiiso  44845  tz6.12-afv  47938  tz6.12-afv2  48005  odz2prm2pw  48343  lighneallem3  48387  lighneallem4b  48389  lindslinindsimp2lem5  49270  nnolog2flm1  49398  2itscp  49589  oppcmndclem  49823