nsyl4 Show Code edit
## Negated Syllogism
thm (nsyl4 () (1 (-> ph ps) 2 (-> (-. ph) ch)) (-> (-. ch) ps)
2 con1i 1 syl)
(-> (-. ch) ps)
edit