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