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  2150  camestros  2154  calemes  2161  calemos  2164  unssin  3403  inssun  3404  onsucelsucexmid  4567  funun  5303  pwuninel2  6349  swoer  6629  swoord1  6630  swoord2  6631  ssfirab  7006  djune  7153  exmidaclem  7291  sucpw1nss3  7318  onntri35  7320  onntri45  7324  elnnz  9353  lbioog  10005  ubioog  10006  fzneuz  10193  fzodisj  10271  infssuzex  10340  fxnn0nninf  10548  zfz1isolemiso  10948  infpnlem1  12553  exmidunben  12668  lgsdir2lem2  15354  2lgslem3  15426