Theorem nsyl 598

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 596	. 2 ⊢ (𝜒 → ¬ 𝜑)
4	3	con2i 597	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  602  jcn  621  pm4.52im  847  intnand  884  intnanrd  885  camestres  2065  camestros  2069  calemes  2076  calemos  2079  unssin  3262  inssun  3263  onsucelsucexmid  4383  funun  5103  pwuninel2  6109  swoer  6387  swoord1  6388  swoord2  6389  ssfirab  6750  djune  6878  elnnz  8916  lbioog  9537  ubioog  9538  fzneuz  9722  fzodisj  9796  fxnn0nninf  10052  zfz1isolemiso  10423  infssuzex  11437  exmidunben  11731