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  6111  xpexr  7919  bropopvvv  8094  bropfvvvv  8096  reldmtpos  8238  zeo  12684  rpneg  13046  xrlttri  13160  difreicc  13506  pfxnd0  14711  nn0o1gt2  16405  cshwshashlem1  17120  gsumcom3fi  19965  gsumbagdiag  21896  psrass1lem  21897  cfinufil  23871  2sq2  27401  2sqnn0  27406  sltlpss  27876  sizusglecusg  29448  iswspthsnon  29843  clwlkclwwlklem2a4  29983  frgrncvvdeqlem8  30292  chirredi  32380  gsummpt2co  33047  truae  34279  bj-sngltag  37006  itg2addnclem  37700  itg2addnclem3  37702  cdleme32e  40469  dflim5  43320  ntrneiiso  44082  tz6.12-afv  47169  tz6.12-afv2  47236  odz2prm2pw  47544  lighneallem3  47588  lighneallem4b  47590  lindslinindsimp2lem5  48405  nnolog2flm1  48537  2itscp  48728  oppcmndclem  48959