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