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