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  4626  funun  5368  opabn1stprc  6353  pwuninel2  6443  swoer  6725  swoord1  6726  swoord2  6727  ssfirab  7123  djune  7271  exmidaclem  7416  sucpw1nss3  7446  onntri35  7448  onntri45  7452  elnnz  9482  lbioog  10141  ubioog  10142  fzneuz  10329  fzodisj  10408  fzodisjsn  10412  infssuzex  10486  fxnn0nninf  10694  zfz1isolemiso  11096  swrd0g  11234  infpnlem1  12925  exmidunben  13040  lgsdir2lem2  15751  2lgslem3  15823  vdegp1aid  16125