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