syl3anc Show Code edit
# A syllogism inference combined with contraction.
thm (syl3anc () (syl3anc.1 (-> (/\/\ ph ps ch) th) syl3anc.2 (-> ta ph) syl3anc.3 (-> ta ps) syl3anc.4 (-> ta ch)) (-> ta th) syl3anc.2 syl3anc.3 syl3anc.4 3jca syl3anc.1 syl)
(-> ta th)
edit