nsyli Show Code edit
## Negated Syllogism
thm (nsyli () (1 (-> ph (-> ps ch)) 2 (-> th (-. ch))) (-> ph (-> th (-. ps)))
1 con3d 2 syl5)
(-> ph (-> th (-. ps)))
edit