Theorem pm2.24d 151

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.5g  168  impimprbi  828  asymref2  6136  xpexr  7941  bropopvvv  8116  bropfvvvv  8118  reldmtpos  8260  zeo  12706  rpneg  13068  xrlttri  13182  difreicc  13525  pfxnd0  14727  nn0o1gt2  16419  cshwshashlem1  17134  gsumcom3fi  19998  gsumbagdiag  21952  psrass1lem  21953  cfinufil  23937  2sq2  27478  2sqnn0  27483  sltlpss  27946  sizusglecusg  29482  iswspthsnon  29877  clwlkclwwlklem2a4  30017  frgrncvvdeqlem8  30326  chirredi  32414  gsummpt2co  33052  truae  34245  bj-sngltag  36985  itg2addnclem  37679  itg2addnclem3  37681  cdleme32e  40448  dflim5  43347  ntrneiiso  44109  tz6.12-afv  47190  tz6.12-afv2  47257  odz2prm2pw  47555  lighneallem3  47599  lighneallem4b  47601  lindslinindsimp2lem5  48384  nnolog2flm1  48516  2itscp  48707  oppcmndclem  48920