sylan9r Show Code edit
# Nested syllogism inference conjoining dissimilar antecedents.
## Syllogism
thm (sylan9r () (sylan9r.1 (-> ph (-> ps ch)) sylan9r.2 (-> th (-> ch ta))) (-> (/\ th ph) (-> ps ta)) sylan9r.1 sylan9r.2 syl9r imp)
(-> (/\ th ph) (-> ps ta))
edit