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