imim2i Show Code edit
## Syllogism
##
## The theorem imim2 written as an inference.
##
##
## (-> [ ph ] [ ps)
## (-> (-> ch [ ph ] ) (-> ch [ ps))
##
thm (imim2i () (1 (-> ph ps)) (-> (-> ch ph) (-> ch ps))
1 ch a1i a2i)
(-> (-> ch ph) (-> ch ps))
edit