syl6bb Show Code edit
# A syllogism inference from two biconditionals.
## Syllogism
thm (syl6bb () (syl6bb.1 (-> ph (<-> ps ch)) syl6bb.2 (<-> ch th)) (-> ph (<-> ps th)) syl6bb.1 syl6bb.2 ph a1i bitrd)
(-> ph (<-> ps th))
edit