Theorem nsyl 600

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 598	. 2 |- ( ch -> -. ph )
4	3	con2i 599	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 586  ax-in2 587

This theorem is referenced by:  con3i  604  jcn  624  pm4.52im  722  intnand  899  intnanrd  900  camestres  2080  camestros  2084  calemes  2091  calemos  2094  unssin  3281  inssun  3282  onsucelsucexmid  4405  funun  5125  pwuninel2  6133  swoer  6411  swoord1  6412  swoord2  6413  ssfirab  6774  djune  6915  exmidaclem  7012  elnnz  8965  lbioog  9586  ubioog  9587  fzneuz  9771  fzodisj  9845  fxnn0nninf  10101  zfz1isolemiso  10472  infssuzex  11487  exmidunben  11781