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  4578  funun  5315  pwuninel2  6368  swoer  6648  swoord1  6649  swoord2  6650  ssfirab  7033  djune  7180  exmidaclem  7320  sucpw1nss3  7347  onntri35  7349  onntri45  7353  elnnz  9382  lbioog  10035  ubioog  10036  fzneuz  10223  fzodisj  10302  infssuzex  10376  fxnn0nninf  10584  zfz1isolemiso  10984  swrd0g  11113  infpnlem1  12682  exmidunben  12797  lgsdir2lem2  15506  2lgslem3  15578