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  752  intnand  933  intnanrd  934  intn3an1d  1368  intn3an2d  1369  intn3an3d  1370  camestres  2161  camestros  2165  calemes  2172  calemos  2175  unssin  3420  inssun  3421  onsucelsucexmid  4596  funun  5334  pwuninel2  6391  swoer  6671  swoord1  6672  swoord2  6673  ssfirab  7059  djune  7206  exmidaclem  7351  sucpw1nss3  7381  onntri35  7383  onntri45  7387  elnnz  9417  lbioog  10070  ubioog  10071  fzneuz  10258  fzodisj  10337  fzodisjsn  10341  infssuzex  10413  fxnn0nninf  10621  zfz1isolemiso  11021  swrd0g  11151  infpnlem1  12797  exmidunben  12912  lgsdir2lem2  15621  2lgslem3  15693