syl3an Show Code edit
# A triple syllogism inference.
thm (syl3an () (syl3an.1 (-> (/\/\ ph ps ch) th) syl3an.2 (-> ta ph) syl3an.3 (-> et ps) syl3an.4 (-> ze ch)) (-> (/\/\ ta et ze) th) syl3an.2 syl3an.3 syl3an.4 3anim123i syl3an.1 syl)
(-> (/\/\ ta et ze) th)
edit