sylancl Show Code edit
## Syllogism
thm (sylancl () (sylancl.1 (-> (/\ ph ps) ch) sylancl.2 (-> th ph) sylancl.3 ps) (-> th ch) sylancl.1 sylancl.2 sylancl.3 th a1i sylanc)
(-> th ch)
edit