syl5ibr Show Code edit
## Syllogism
thm (syl5ibr () (HIMP (-> ph (-> ps ch)) HEQ (<-> ps th)) (-> ph (-> th ch))
HIMP
(-> ph (-> ps ch))
HEQ bicomi
(<-> th ps)
syl5ib
(-> ph (-> th ch))
)
edit