Theorem nsyl 629

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  633  pm4.52im  752  intnand  933  intnanrd  934  intn3an1d  1368  intn3an2d  1369  intn3an3d  1370  camestres  2160  camestros  2164  calemes  2171  calemos  2174  unssin  3416  inssun  3417  onsucelsucexmid  4585  funun  5323  pwuninel2  6380  swoer  6660  swoord1  6661  swoord2  6662  ssfirab  7047  djune  7194  exmidaclem  7335  sucpw1nss3  7362  onntri35  7364  onntri45  7368  elnnz  9397  lbioog  10050  ubioog  10051  fzneuz  10238  fzodisj  10317  fzodisjsn  10321  infssuzex  10393  fxnn0nninf  10601  zfz1isolemiso  11001  swrd0g  11131  infpnlem1  12752  exmidunben  12867  lgsdir2lem2  15576  2lgslem3  15648