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  6070  xpexr  7858  bropopvvv  8030  bropfvvvv  8032  reldmtpos  8174  zeo  12580  rpneg  12945  xrlttri  13059  difreicc  13405  pfxnd0  14613  nn0o1gt2  16310  cshwshashlem1  17025  gsumcom3fi  19876  gsumbagdiag  21856  psrass1lem  21857  cfinufil  23831  2sq2  27360  2sqnn0  27365  sltlpss  27840  sizusglecusg  29427  iswspthsnon  29819  clwlkclwwlklem2a4  29959  frgrncvvdeqlem8  30268  chirredi  32356  gsummpt2co  33014  truae  34209  bj-sngltag  36956  itg2addnclem  37650  itg2addnclem3  37652  cdleme32e  40424  dflim5  43302  ntrneiiso  44064  tz6.12-afv  47158  tz6.12-afv2  47225  odz2prm2pw  47548  lighneallem3  47592  lighneallem4b  47594  lindslinindsimp2lem5  48435  nnolog2flm1  48563  2itscp  48754  oppcmndclem  48990