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  9604  lbioog  10265  ubioog  10266  fzneuz  10457  fzodisj  10536  fzodisjsn  10540  infssuzex  10615  fxnn0nninf  10825  zfz1isolemiso  11236  swrd0g  11377  infpnlem1  13082  ballotfilemfp1  13175  ballotfilem4  13185  ballotfilemirc  13219  exmidunben  13261  lgsdir2lem2  16014  2lgslem3  16086  vdegp1aid  16421