syld3an1 Show Code edit
# A syllogism inference.
thm (syld3an1 () (syl3an.1 (-> (/\/\ ph ps ch) th) syld3an1.2 (-> (/\/\ ta ps ch) ph)) (-> (/\/\ ta ps ch) th) syl3an.1 3com13 syld3an1.2 3com13 syld3an3 3com13)
(-> (/\/\ ta ps ch) th)
edit