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  7863  bropopvvv  8035  bropfvvvv  8037  reldmtpos  8179  zeo  12583  rpneg  12944  xrlttri  13058  difreicc  13405  pfxnd0  14617  nn0o1gt2  16313  cshwshashlem1  17028  gsumcom3fi  19913  gsumbagdiag  21892  psrass1lem  21893  cfinufil  23877  2sq2  27405  2sqnn0  27410  ltslpss  27909  sizusglecusg  29542  iswspthsnon  29934  clwlkclwwlklem2a4  30077  frgrncvvdeqlem8  30386  chirredi  32474  gsummpt2co  33134  truae  34413  bj-sngltag  37197  itg2addnclem  37885  itg2addnclem3  37887  cdleme32e  40784  dflim5  43649  ntrneiiso  44410  tz6.12-afv  47496  tz6.12-afv2  47563  odz2prm2pw  47886  lighneallem3  47930  lighneallem4b  47932  lindslinindsimp2lem5  48785  nnolog2flm1  48913  2itscp  49104  oppcmndclem  49339