Theorem nsyl 628

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  632  pm4.52im  750  intnand  931  intnanrd  932  camestres  2131  camestros  2135  calemes  2142  calemos  2145  unssin  3376  inssun  3377  onsucelsucexmid  4531  funun  5262  pwuninel2  6285  swoer  6565  swoord1  6566  swoord2  6567  ssfirab  6935  djune  7079  exmidaclem  7209  sucpw1nss3  7236  onntri35  7238  onntri45  7242  elnnz  9265  lbioog  9915  ubioog  9916  fzneuz  10103  fzodisj  10180  fxnn0nninf  10440  zfz1isolemiso  10821  infssuzex  11952  infpnlem1  12359  exmidunben  12429  lgsdir2lem2  14515