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