syl5d Show Code edit
## Syllogism Deduction
thm (syl5d () (1 (-> ph (-> ps (-> ch th))) 2 (-> ph (-> ta ch)))
(-> ph (-> ps (-> ta th)))
2 ps a1d 1 syldd)
(-> ph (-> ps (-> ta th)))
edit