nsyl4t Show Code edit
## Negated Syllogism
thm (nsyl4t () () (-> (-> ph ps) (-> (-> (-. ph) ch) (-> (-. ch) ps)))
ph ch con1 (-. ch) ph ps imim1 syl com12)
(-> (-> ph ps) (-> (-> (-. ph) ch) (-> (-. ch) ps)))
edit