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