Theorem nsyl 629

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  633  pm4.52im  751  intnand  932  intnanrd  933  camestres  2147  camestros  2151  calemes  2158  calemos  2161  unssin  3398  inssun  3399  onsucelsucexmid  4562  funun  5298  pwuninel2  6335  swoer  6615  swoord1  6616  swoord2  6617  ssfirab  6990  djune  7137  exmidaclem  7268  sucpw1nss3  7295  onntri35  7297  onntri45  7301  elnnz  9327  lbioog  9979  ubioog  9980  fzneuz  10167  fzodisj  10245  fxnn0nninf  10510  zfz1isolemiso  10910  infssuzex  12086  infpnlem1  12497  exmidunben  12583  lgsdir2lem2  15145