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