sylancb Show Code edit
## Syllogism & Contraction
thm (sylancb () (sylancb.1 (-> (/\ ph ps) ch) sylancb.2 (<-> th ph) sylancb.3 (<-> th ps)) (-> th ch) sylancb.1 sylancb.2 sylancb.3 syl2anb anidms)
(-> th ch)
edit