syl6 Show Code edit
## A syllogism rule of inference
##
## The second premise is used to replace the consequent of the first premise.
##
thm (syl6 () (1 (-> ph (-> ps ch)) 2 (-> ch th)) (-> ph (-> ps th))
1 2 ps imim2i syl)
(-> ph (-> ps th))
edit