Theorem nsyl 558

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  562  pm4.52im  803  intnand  840  intnanrd  841  camestres  2005  camestros  2009  calemes  2016  calemos  2019  pssn2lp  3045  unssin  3176  inssun  3177  onsucelsucexmid  4255  funun  4944  pwuninel2  5897  swoer  6134  swoord1  6135  swoord2  6136  elnnz  8255  lbioog  8782  ubioog  8783  fzneuz  8963  fzodisj  9034