Theorem nsyl 591

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 589	. 2 |- ( ch -> -. ph )
4	3	con2i 590	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 577  ax-in2 578

This theorem is referenced by:  con3i  595  pm4.52im  837  intnand  874  intnanrd  875  camestres  2047  camestros  2051  calemes  2058  calemos  2061  unssin  3210  inssun  3211  onsucelsucexmid  4281  funun  4974  pwuninel2  5931  swoer  6200  swoord1  6201  swoord2  6202  elnnz  8442  lbioog  9012  ubioog  9013  fzneuz  9194  fzodisj  9264  infssuzex  10489