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  6069  xpexr  7854  bropopvvv  8026  bropfvvvv  8028  reldmtpos  8170  zeo  12565  rpneg  12930  xrlttri  13044  difreicc  13390  pfxnd0  14602  nn0o1gt2  16298  cshwshashlem1  17013  gsumcom3fi  19897  gsumbagdiag  21874  psrass1lem  21875  cfinufil  23849  2sq2  27377  2sqnn0  27382  sltlpss  27859  sizusglecusg  29449  iswspthsnon  29841  clwlkclwwlklem2a4  29984  frgrncvvdeqlem8  30293  chirredi  32381  gsummpt2co  33035  truae  34263  bj-sngltag  37034  itg2addnclem  37717  itg2addnclem3  37719  cdleme32e  40550  dflim5  43427  ntrneiiso  44189  tz6.12-afv  47278  tz6.12-afv2  47345  odz2prm2pw  47668  lighneallem3  47712  lighneallem4b  47714  lindslinindsimp2lem5  48568  nnolog2flm1  48696  2itscp  48887  oppcmndclem  49123