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