Theorem nsyl 631

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  con3i  635  pm4.52im  755  intnand  936  intnanrd  937  intn3an1d  1390  intn3an2d  1391  intn3an3d  1392  camestres  2183  camestros  2187  calemes  2194  calemos  2197  unssin  3444  inssun  3445  onsucelsucexmid  4624  funun  5366  opabn1stprc  6351  pwuninel2  6441  swoer  6723  swoord1  6724  swoord2  6725  ssfirab  7119  djune  7266  exmidaclem  7411  sucpw1nss3  7441  onntri35  7443  onntri45  7447  elnnz  9477  lbioog  10136  ubioog  10137  fzneuz  10324  fzodisj  10403  fzodisjsn  10407  infssuzex  10481  fxnn0nninf  10689  zfz1isolemiso  11090  swrd0g  11228  infpnlem1  12919  exmidunben  13034  lgsdir2lem2  15745  2lgslem3  15817