syl2anbr Show Code edit
## Double Syllogism
thm (syl2anbr () (sylan.1 (-> (/\ ph ps) ch) syl2anbr.2 (<-> ph th) syl2anbr.3 (<-> ps ta)) (-> (/\ th ta) ch) sylan.1 syl2anbr.2 sylanbr syl2anbr.3 sylan2br)
(-> (/\ th ta) ch)
edit