Theorem nsyl 633

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  637  pm4.52im  758  intnand  939  intnanrd  940  intn3an1d  1393  intn3an2d  1394  intn3an3d  1395  camestres  2188  camestros  2192  calemes  2199  calemos  2202  unssin  3464  inssun  3465  onsucelsucexmid  4657  funun  5402  opabn1stprc  6402  pwuninel2  6526  swoer  6808  swoord1  6809  swoord2  6810  ssfirab  7210  djune  7382  exmidaclem  7528  sucpw1nss3  7558  onntri35  7560  onntri45  7564  elnnz  9607  lbioog  10268  ubioog  10269  fzneuz  10460  fzodisj  10539  fzodisjsn  10543  infssuzex  10618  fxnn0nninf  10828  zfz1isolemiso  11239  swrd0g  11380  infpnlem1  13086  ballotfilemfp1  13179  ballotfilem4  13189  ballotfilemirc  13223  exmidunben  13265  lgsdir2lem2  16032  2lgslem3  16104  vdegp1aid  16439