Theorem nsyl 633

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  637  pm4.52im  758  intnand  939  intnanrd  940  intn3an1d  1393  intn3an2d  1394  intn3an3d  1395  camestres  2186  camestros  2190  calemes  2197  calemos  2200  unssin  3459  inssun  3460  onsucelsucexmid  4651  funun  5396  opabn1stprc  6388  pwuninel2  6512  swoer  6794  swoord1  6795  swoord2  6796  ssfirab  7196  djune  7368  exmidaclem  7514  sucpw1nss3  7544  onntri35  7546  onntri45  7550  elnnz  9586  lbioog  10245  ubioog  10246  fzneuz  10434  fzodisj  10513  fzodisjsn  10517  infssuzex  10592  fxnn0nninf  10800  zfz1isolemiso  11207  swrd0g  11348  infpnlem1  13053  exmidunben  13169  lgsdir2lem2  15894  2lgslem3  15966  vdegp1aid  16301