sylbir Show Code edit
## Syllogism
thm (sylbir () (1 (<-> ps ph) 2 (-> ps ch)) (-> ph ch)
1 biimpri 2 syl)
(-> ph ch)
edit