syl3an3br Show Code edit
# A syllogism inference.
thm (syl3an3br () (syl3an.1 (-> (/\/\ ph ps ch) th) syl3an3br.2 (<-> ch ta)) (-> (/\/\ ph ps ta) th) syl3an.1 syl3an3br.2 biimpri syl3an3)
(-> (/\/\ ph ps ta) th)
edit