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