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  7418  exmidaclem  7564  sucpw1nss3  7594  onntri35  7596  onntri45  7600  elnnz  9656  lbioog  10317  ubioog  10318  fzneuz  10510  fzodisj  10589  fzodisjsn  10593  infssuzex  10668  fxnn0nninf  10878  zfz1isolemiso  11293  swrd0g  11434  infpnlem1  13140  ballotfilemfp1  13233  ballotfilem4  13243  ballotfilemirc  13277  exmidunben  13319  lgsdir2lem2  16160  2lgslem3  16232  vdegp1aid  16567