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