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 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced 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  4675  funun  5420  opabn1stprc  6423  pwuninel2  6547  swoer  6829  swoord1  6830  swoord2  6831  ssfirab  7238  djune  7412  exmidaclem  7558  sucpw1nss3  7588  onntri35  7590  onntri45  7594  elnnz  9637  lbioog  10298  ubioog  10299  fzneuz  10491  fzodisj  10570  fzodisjsn  10574  infssuzex  10649  fxnn0nninf  10859  zfz1isolemiso  11274  swrd0g  11415  infpnlem1  13121  ballotfilemfp1  13214  ballotfilem4  13224  ballotfilemirc  13258  exmidunben  13300  lgsdir2lem2  16131  2lgslem3  16203  vdegp1aid  16538