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