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  758  intnand  939  intnanrd  940  intn3an1d  1393  intn3an2d  1394  intn3an3d  1395  camestres  2185  camestros  2189  calemes  2196  calemos  2199  unssin  3448  inssun  3449  onsucelsucexmid  4634  funun  5378  opabn1stprc  6367  pwuninel2  6491  swoer  6773  swoord1  6774  swoord2  6775  ssfirab  7172  djune  7320  exmidaclem  7466  sucpw1nss3  7496  onntri35  7498  onntri45  7502  elnnz  9532  lbioog  10191  ubioog  10192  fzneuz  10379  fzodisj  10458  fzodisjsn  10462  infssuzex  10537  fxnn0nninf  10745  zfz1isolemiso  11147  swrd0g  11288  infpnlem1  12993  exmidunben  13108  lgsdir2lem2  15828  2lgslem3  15900  vdegp1aid  16235