Theorem nsyl 637

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  con3i  641  pm4.52im  762  intnand  943  intnanrd  944  intn3an1d  1397  intn3an2d  1398  intn3an3d  1399  camestres  2192  camestros  2196  calemes  2203  calemos  2206  unssin  3470  inssun  3471  onsucelsucexmid  4677  funun  5422  opabn1stprc  6429  pwuninel2  6553  swoer  6835  swoord1  6836  swoord2  6837  ssfirab  7244  djune  7419  exmidaclem  7565  sucpw1nss3  7595  onntri35  7597  onntri45  7601  elnnz  9659  lbioog  10326  ubioog  10327  fzneuz  10519  fzodisj  10598  fzodisjsn  10602  infssuzex  10677  fxnn0nninf  10890  zfz1isolemiso  11306  swrd0g  11447  infpnlem1  13160  ballotfilemfp1  13282  ballotfilem4  13292  ballotfilemirc  13326  exmidunben  13368  ppiprm  16181  chtprm  16183  lgsdir2lem2  16270  2lgslem3  16342  vdegp1aid  16677