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  4679  funun  5425  opabn1stprc  6433  pwuninel2  6558  swoer  6840  swoord1  6841  swoord2  6842  ssfirab  7250  djune  7425  exmidaclem  7571  sucpw1nss3  7601  onntri35  7603  onntri45  7607  elnnz  9664  lbioog  10332  ubioog  10333  fzneuz  10525  fzodisj  10604  fzodisjsn  10608  infssuzex  10683  fxnn0nninf  10897  zfz1isolemiso  11313  swrd0g  11454  infpnlem1  13167  ballotfilemfp1  13289  ballotfilem4  13299  ballotfilemirc  13333  exmidunben  13375  gsumresfi  14263  mvrf1fi  15231  ppiprm  16292  chtprm  16294  lgsdir2lem2  16386  2lgslem3  16458  vdegp1aid  16793