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  6111  xpexr  7930  bropopvvv  8101  bropfvvvv  8103  reldmtpos  8251  zeo  12785  rpneg  13154  xrlttri  13268  difreicc  13615  pfxnd0  14838  nn0o1gt2  16551  cshwshashlem1  17273  gsumcom3fi  20193  gsumbagdiag  22240  psrass1lem  22241  cfinufil  24247  2sq2  27760  2sqnn0  27765  ltslpss  28294  sizusglecusg  30044  iswspthsnon  30445  clwlkclwwlklem2a4  30588  frgrncvvdeqlem8  30907  chirredi  32996  gsummpt2co  33609  truae  34876  soinfdom  35717  bj-sngltag  37896  itg2addnclem  38590  itg2addnclem3  38592  cdleme32e  41503  dflim5  44331  ntrneiiso  45091  tz6.12-afv  48243  tz6.12-afv2  48310  odz2prm2pw  48648  lighneallem3  48692  lighneallem4b  48694  lindslinindsimp2lem5  49574  nnolog2flm1  49702  2itscp  49893  oppcmndclem  50125