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