Theorem nsyl 617

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

This theorem is referenced by:  con3i  621  jcn  641  pm4.52im  739  intnand  916  intnanrd  917  camestres  2102  camestros  2106  calemes  2113  calemos  2116  unssin  3310  inssun  3311  onsucelsucexmid  4440  funun  5162  pwuninel2  6172  swoer  6450  swoord1  6451  swoord2  6452  ssfirab  6815  djune  6956  exmidaclem  7057  elnnz  9057  lbioog  9689  ubioog  9690  fzneuz  9874  fzodisj  9948  fxnn0nninf  10204  zfz1isolemiso  10575  infssuzex  11631  exmidunben  11928