sylbid Show Code edit
## Syllogism
thm (sylbid () (1 (-> ph (<-> ps ch)) 2 (-> ph (-> ch th))) (-> ph (-> ps th))
1 biimpd 2 syld)
(-> ph (-> ps th))
edit