imim1 Show Code edit
# a.k.a. sylt
## Syllogism (Closed Form)
thm (imim1 () () (-> (-> ph ps) (-> (-> ps ch) (-> ph ch)))
ps ch ph imim2 com12)
(-> (-> ph ps) (-> (-> ps ch) (-> ph ch)))
edit