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  7293  sucpw1nss3  7320  onntri35  7322  onntri45  7326  elnnz  9355  lbioog  10007  ubioog  10008  fzneuz  10195  fzodisj  10273  infssuzex  10342  fxnn0nninf  10550  zfz1isolemiso  10950  infpnlem1  12555  exmidunben  12670  lgsdir2lem2  15378  2lgslem3  15450