sylan2d Show Code edit
## Syllogism
thm (sylan2d () (sylan2d.1 (-> ph (-> (/\ ps ch) th)) sylan2d.2 (-> ph (-> ta ch))) (-> ph (-> (/\ ps ta) th)) sylan2d.1 ancomsd sylan2d.2 syland ancomsd)
(-> ph (-> (/\ ps ta) th))
edit