sylan9bbr Show Code edit
# Nested syllogism inference conjoining dissimilar antecedents.
## Syllogism
thm (sylan9bbr () (sylan9bbr.1 (-> ph (<-> ps ch)) sylan9bbr.2 (-> th (<-> ch ta))) (-> (/\ th ph) (<-> ps ta)) sylan9bbr.1 sylan9bbr.2 sylan9bb ancoms)
(-> (/\ th ph) (<-> ps ta))
edit