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	|- ( ph -> -. ps )
nsyl.2	|- ( ch -> ps )

Assertion

Ref	Expression
nsyl	|- ( ph -> -. ch )

Proof of Theorem nsyl

Step	Hyp	Ref	Expression
1		nsyl.1	. . 3 |- ( ph -> -. ps )
2		nsyl.2	. . 3 |- ( ch -> ps )
3	1, 2	nsyl3 627	. 2 |- ( ch -> -. ph )
4	3	con2i 628	1 |- ( ph -> -. ch )

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  751  intnand  932  intnanrd  933  camestres  2147  camestros  2151  calemes  2158  calemos  2161  unssin  3399  inssun  3400  onsucelsucexmid  4563  funun  5299  pwuninel2  6337  swoer  6617  swoord1  6618  swoord2  6619  ssfirab  6992  djune  7139  exmidaclem  7270  sucpw1nss3  7297  onntri35  7299  onntri45  7303  elnnz  9330  lbioog  9982  ubioog  9983  fzneuz  10170  fzodisj  10248  fxnn0nninf  10513  zfz1isolemiso  10913  infssuzex  12089  infpnlem1  12500  exmidunben  12586  lgsdir2lem2  15186  2lgslem3  15258