Theorem nsyl 617

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  621  pm4.52im  739  intnand  916  intnanrd  917  camestres  2104  camestros  2108  calemes  2115  calemos  2118  unssin  3315  inssun  3316  onsucelsucexmid  4445  funun  5167  pwuninel2  6179  swoer  6457  swoord1  6458  swoord2  6459  ssfirab  6822  djune  6963  exmidaclem  7064  elnnz  9064  lbioog  9696  ubioog  9697  fzneuz  9881  fzodisj  9955  fxnn0nninf  10211  zfz1isolemiso  10582  infssuzex  11642  exmidunben  11939