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  829  asymref2  6075  xpexr  7862  bropopvvv  8034  bropfvvvv  8036  reldmtpos  8178  zeo  12582  rpneg  12943  xrlttri  13057  difreicc  13404  pfxnd0  14616  nn0o1gt2  16312  cshwshashlem1  17027  gsumcom3fi  19912  gsumbagdiag  21891  psrass1lem  21892  cfinufil  23876  2sq2  27404  2sqnn0  27409  sltlpss  27890  sizusglecusg  29520  iswspthsnon  29912  clwlkclwwlklem2a4  30055  frgrncvvdeqlem8  30364  chirredi  32452  gsummpt2co  33112  truae  34381  bj-sngltag  37159  itg2addnclem  37843  itg2addnclem3  37845  cdleme32e  40742  dflim5  43607  ntrneiiso  44368  tz6.12-afv  47455  tz6.12-afv2  47522  odz2prm2pw  47845  lighneallem3  47889  lighneallem4b  47891  lindslinindsimp2lem5  48744  nnolog2flm1  48872  2itscp  49063  oppcmndclem  49298