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  6093  xpexr  7897  bropopvvv  8072  bropfvvvv  8074  reldmtpos  8216  zeo  12627  rpneg  12992  xrlttri  13106  difreicc  13452  pfxnd0  14660  nn0o1gt2  16358  cshwshashlem1  17073  gsumcom3fi  19916  gsumbagdiag  21847  psrass1lem  21848  cfinufil  23822  2sq2  27351  2sqnn0  27356  sltlpss  27826  sizusglecusg  29398  iswspthsnon  29793  clwlkclwwlklem2a4  29933  frgrncvvdeqlem8  30242  chirredi  32330  gsummpt2co  32995  truae  34240  bj-sngltag  36978  itg2addnclem  37672  itg2addnclem3  37674  cdleme32e  40446  dflim5  43325  ntrneiiso  44087  tz6.12-afv  47178  tz6.12-afv2  47245  odz2prm2pw  47568  lighneallem3  47612  lighneallem4b  47614  lindslinindsimp2lem5  48455  nnolog2flm1  48583  2itscp  48774  oppcmndclem  49010