Theorem nsyl 618

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 616	. 2 |- ( ch -> -. ph )
4	3	con2i 617	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 604  ax-in2 605

This theorem is referenced by:  con3i  622  pm4.52im  740  intnand  921  intnanrd  922  camestres  2118  camestros  2122  calemes  2129  calemos  2132  unssin  3356  inssun  3357  onsucelsucexmid  4501  funun  5226  pwuninel2  6241  swoer  6520  swoord1  6521  swoord2  6522  ssfirab  6890  djune  7034  exmidaclem  7155  sucpw1nss3  7182  onntri35  7184  onntri45  7188  elnnz  9192  lbioog  9840  ubioog  9841  fzneuz  10026  fzodisj  10103  fxnn0nninf  10363  zfz1isolemiso  10738  infssuzex  11867  exmidunben  12296