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