Theorem nsyl 618

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  622  pm4.52im  740  intnand  921  intnanrd  922  camestres  2119  camestros  2123  calemes  2130  calemos  2133  unssin  3361  inssun  3362  onsucelsucexmid  4507  funun  5232  pwuninel2  6250  swoer  6529  swoord1  6530  swoord2  6531  ssfirab  6899  djune  7043  exmidaclem  7164  sucpw1nss3  7191  onntri35  7193  onntri45  7197  elnnz  9201  lbioog  9849  ubioog  9850  fzneuz  10036  fzodisj  10113  fxnn0nninf  10373  zfz1isolemiso  10752  infssuzex  11882  infpnlem1  12289  exmidunben  12359  lgsdir2lem2  13570