Theorem nsyl 590

Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)

Hypotheses

Ref	Expression
nsyl.1	⊢ (𝜑 → ¬ 𝜓)
nsyl.2	⊢ (𝜒 → 𝜓)

Assertion

Ref	Expression
nsyl	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem nsyl

Step	Hyp	Ref	Expression
1		nsyl.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2		nsyl.2	. . 3 ⊢ (𝜒 → 𝜓)
3	1, 2	nsyl3 588	. 2 ⊢ (𝜒 → ¬ 𝜑)
4	3	con2i 589	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 576  ax-in2 577

This theorem is referenced by:  con3i  594  pm4.52im  836  intnand  873  intnanrd  874  camestres  2046  camestros  2050  calemes  2057  calemos  2060  unssin  3203  inssun  3204  onsucelsucexmid  4273  funun  4964  pwuninel2  5920  swoer  6157  swoord1  6158  swoord2  6159  elnnz  8361  lbioog  8936  ubioog  8937  fzneuz  9118  fzodisj  9187  infssuzex  10345