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