imim1i Show Code edit
## Syllogism
##
## The theorem imim1 written as an inference.
##
thm (imim1i () (1 (-> ph ps)) (-> (-> ps ch) (-> ph ch))
1 ph ps ch imim1 ax-mp)
(-> (-> ps ch) (-> ph ch))
edit