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