Theorem pm2.24d 152

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.5g  169  impimprbi  842  asymref2  6115  xpexr  7918  bropopvvv  8090  bropfvvvv  8092  reldmtpos  8235  zeo  12710  rpneg  13078  xrlttri  13192  difreicc  13539  pfxnd0  14760  nn0o1gt2  16475  cshwshashlem1  17191  gsumcom3fi  20107  gsumbagdiag  22148  psrass1lem  22149  cfinufil  24155  2sq2  27667  2sqnn0  27672  ltslpss  28171  sizusglecusg  29909  iswspthsnon  30310  clwlkclwwlklem2a4  30453  frgrncvvdeqlem8  30772  chirredi  32861  gsummpt2co  33475  truae  34741  bj-sngltag  37714  itg2addnclem  38407  itg2addnclem3  38409  cdleme32e  41305  dflim5  44157  ntrneiiso  44918  tz6.12-afv  48048  tz6.12-afv2  48115  odz2prm2pw  48453  lighneallem3  48497  lighneallem4b  48499  lindslinindsimp2lem5  49379  nnolog2flm1  49507  2itscp  49698  oppcmndclem  49930