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  3443  inssun  3444  onsucelsucexmid  4623  funun  5365  opabn1stprc  6350  pwuninel2  6439  swoer  6721  swoord1  6722  swoord2  6723  ssfirab  7114  djune  7261  exmidaclem  7406  sucpw1nss3  7436  onntri35  7438  onntri45  7442  elnnz  9472  lbioog  10126  ubioog  10127  fzneuz  10314  fzodisj  10393  fzodisjsn  10397  infssuzex  10470  fxnn0nninf  10678  zfz1isolemiso  11079  swrd0g  11213  infpnlem1  12903  exmidunben  13018  lgsdir2lem2  15729  2lgslem3  15801