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