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  2143  camestros  2147  calemes  2154  calemos  2157  unssin  3389  inssun  3390  onsucelsucexmid  4547  funun  5279  pwuninel2  6308  swoer  6588  swoord1  6589  swoord2  6590  ssfirab  6963  djune  7108  exmidaclem  7238  sucpw1nss3  7265  onntri35  7267  onntri45  7271  elnnz  9294  lbioog  9945  ubioog  9946  fzneuz  10133  fzodisj  10210  fxnn0nninf  10471  zfz1isolemiso  10854  infssuzex  11985  infpnlem1  12394  exmidunben  12480  lgsdir2lem2  14908