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