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  2159  camestros  2163  calemes  2170  calemos  2173  unssin  3412  inssun  3413  onsucelsucexmid  4579  funun  5316  pwuninel2  6370  swoer  6650  swoord1  6651  swoord2  6652  ssfirab  7035  djune  7182  exmidaclem  7322  sucpw1nss3  7349  onntri35  7351  onntri45  7355  elnnz  9384  lbioog  10037  ubioog  10038  fzneuz  10225  fzodisj  10304  infssuzex  10378  fxnn0nninf  10586  zfz1isolemiso  10986  swrd0g  11116  infpnlem1  12715  exmidunben  12830  lgsdir2lem2  15539  2lgslem3  15611