sylan9 Show Code edit
# Nested syllogism inference conjoining dissimilar antecedents.
## Syllogism
thm (sylan9 () (sylan9.1 (-> ph (-> ps ch)) sylan9.2 (-> th (-> ch ta))) (-> (/\ ph th) (-> ps ta)) sylan9.1 th adantr sylan9.2 ph adantl syld)
(-> (/\ ph th) (-> ps ta))
edit