Theorem nsyl 623

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  627  pm4.52im  745  intnand  926  intnanrd  927  camestres  2124  camestros  2128  calemes  2135  calemos  2138  unssin  3366  inssun  3367  onsucelsucexmid  4514  funun  5242  pwuninel2  6261  swoer  6541  swoord1  6542  swoord2  6543  ssfirab  6911  djune  7055  exmidaclem  7185  sucpw1nss3  7212  onntri35  7214  onntri45  7218  elnnz  9222  lbioog  9870  ubioog  9871  fzneuz  10057  fzodisj  10134  fxnn0nninf  10394  zfz1isolemiso  10774  infssuzex  11904  infpnlem1  12311  exmidunben  12381  lgsdir2lem2  13724