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  6557  swoer  6839  swoord1  6840  swoord2  6841  ssfirab  7249  djune  7425  exmidaclem  7571  sucpw1nss3  7601  onntri35  7603  onntri45  7607  elnnz  9666  lbioog  10333  ubioog  10334  fzneuz  10526  fzodisj  10605  fzodisjsn  10609  infssuzex  10684  fxnn0nninf  10898  zfz1isolemiso  11314  swrd0g  11455  infpnlem1  13168  ballotfilemfp1  13290  ballotfilem4  13300  ballotfilemirc  13334  exmidunben  13376  gsumresfi  14264  mvrf1fi  15215  ppiprm  16271  chtprm  16273  lgsdir2lem2  16365  2lgslem3  16437  vdegp1aid  16772