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