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