syl6com Show Code edit
## Syllogism & Commute Antecedents
thm (syl6com () (1 (-> ph (-> ps ch)) 2 (-> ch th)) (-> ps (-> ph th))
1 2 syl6 com12)
(-> ps (-> ph th))
edit