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  6105  xpexr  7913  bropopvvv  8084  bropfvvvv  8086  reldmtpos  8229  zeo  12754  rpneg  13123  xrlttri  13237  difreicc  13584  pfxnd0  14805  nn0o1gt2  16518  cshwshashlem1  17234  gsumcom3fi  20154  gsumbagdiag  22201  psrass1lem  22202  cfinufil  24208  2sq2  27723  2sqnn0  27728  ltslpss  28227  sizusglecusg  29977  iswspthsnon  30378  clwlkclwwlklem2a4  30521  frgrncvvdeqlem8  30840  chirredi  32929  gsummpt2co  33542  truae  34809  bj-sngltag  37818  itg2addnclem  38509  itg2addnclem3  38511  cdleme32e  41422  dflim5  44274  ntrneiiso  45035  tz6.12-afv  48165  tz6.12-afv2  48232  odz2prm2pw  48570  lighneallem3  48614  lighneallem4b  48616  lindslinindsimp2lem5  49496  nnolog2flm1  49624  2itscp  49815  oppcmndclem  50047