sylanbr Show Code edit
## Syllogism
thm (sylanbr () (sylan.1 (-> (/\ ph ps) ch) sylanbr.2 (<-> ph th)) (-> (/\ th ps) ch) sylan.1 sylanbr.2 biimpri sylan)
(-> (/\ th ps) ch)
edit