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  2150  camestros  2154  calemes  2161  calemos  2164  unssin  3402  inssun  3403  onsucelsucexmid  4566  funun  5302  pwuninel2  6340  swoer  6620  swoord1  6621  swoord2  6622  ssfirab  6997  djune  7144  exmidaclem  7275  sucpw1nss3  7302  onntri35  7304  onntri45  7308  elnnz  9336  lbioog  9988  ubioog  9989  fzneuz  10176  fzodisj  10254  infssuzex  10323  fxnn0nninf  10531  zfz1isolemiso  10931  infpnlem1  12528  exmidunben  12643  lgsdir2lem2  15270  2lgslem3  15342