syl2an Show Code edit
## Double Syllogism
thm (syl2an () (sylan.1 (-> (/\ ph ps) ch) syl2an.2 (-> th ph) syl2an.3 (-> ta ps)) (-> (/\ th ta) ch) sylan.1 syl2an.2 sylan syl2an.3 sylan2)
(-> (/\ th ta) ch)
edit