sylanc Show Code edit
# A syllogism inference combined with contraction.
## Syllogism & Contraction
thm (sylanc () (sylanc.1 (-> (/\ ph ps) ch) sylanc.2 (-> th ph) sylanc.3 (-> th ps)) (-> th ch) sylanc.1 ex sylanc.2 sylanc.3 sylc)
(-> th ch)
edit