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  757  intnand  938  intnanrd  939  intn3an1d  1392  intn3an2d  1393  intn3an3d  1394  camestres  2185  camestros  2189  calemes  2196  calemos  2199  unssin  3446  inssun  3447  onsucelsucexmid  4628  funun  5371  opabn1stprc  6358  pwuninel2  6448  swoer  6730  swoord1  6731  swoord2  6732  ssfirab  7129  djune  7277  exmidaclem  7423  sucpw1nss3  7453  onntri35  7455  onntri45  7459  elnnz  9489  lbioog  10148  ubioog  10149  fzneuz  10336  fzodisj  10415  fzodisjsn  10419  infssuzex  10494  fxnn0nninf  10702  zfz1isolemiso  11104  swrd0g  11245  infpnlem1  12937  exmidunben  13052  lgsdir2lem2  15764  2lgslem3  15836  vdegp1aid  16171