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