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  826  asymref2  6022  xpexr  7765  bropopvvv  7930  bropfvvvv  7932  reldmtpos  8050  zeo  12406  rpneg  12762  xrlttri  12873  difreicc  13216  pfxnd0  14401  nn0o1gt2  16090  cshwshashlem1  16797  gsumcom3fi  19580  gsumbagdiagOLD  21142  psrass1lemOLD  21143  gsumbagdiag  21145  psrass1lem  21146  cfinufil  23079  2sq2  26581  2sqnn0  26586  sizusglecusg  27830  iswspthsnon  28221  clwlkclwwlklem2a4  28361  frgrncvvdeqlem8  28670  chirredi  30756  gsummpt2co  31308  truae  32211  sltlpss  34087  bj-sngltag  35173  itg2addnclem  35828  itg2addnclem3  35830  cdleme32e  38459  ntrneiiso  41701  tz6.12-afv  44665  tz6.12-afv2  44732  odz2prm2pw  45015  lighneallem3  45059  lighneallem4b  45061  lindslinindsimp2lem5  45803  nnolog2flm1  45936  2itscp  46127