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  842  asymref2  6123  xpexr  7954  bropopvvv  8126  bropfvvvv  8128  reldmtpos  8279  zeo  12812  rpneg  13181  xrlttri  13295  difreicc  13642  pfxnd0  14866  nn0o1gt2  16580  cshwshashlem1  17302  gsumcom3fi  20223  gsumbagdiag  22270  psrass1lem  22271  cfinufil  24277  2sq2  27790  2sqnn0  27795  ltslpss  28324  sizusglecusg  30074  iswspthsnon  30475  clwlkclwwlklem2a4  30618  frgrncvvdeqlem8  30937  chirredi  33026  gsummpt2co  33679  truae  34946  soinfdom  35800  bj-sngltag  38074  itg2addnclem  38781  itg2addnclem3  38783  cdleme32e  41694  dflim5  44523  ntrneiiso  45283  tz6.12-afv  48448  tz6.12-afv2  48515  odz2prm2pw  48853  lighneallem3  48897  lighneallem4b  48899  lindslinindsimp2lem5  49779  nnolog2flm1  49907  2itscp  50098  oppcmndclem  50336