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  6110  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  33651  truae  34918  soinfdom  35759  bj-sngltag  37938  itg2addnclem  38632  itg2addnclem3  38634  cdleme32e  41545  dflim5  44374  ntrneiiso  45134  tz6.12-afv  48286  tz6.12-afv2  48353  odz2prm2pw  48691  lighneallem3  48735  lighneallem4b  48737  lindslinindsimp2lem5  49617  nnolog2flm1  49745  2itscp  49936  oppcmndclem  50168