syl6bi Show Code edit
## Syllogism
thm (syl6bi () (HEQ (-> ph (<-> ps ch)) HIMP (-> ch th)) (-> ph (-> ps th))
HEQ biimpd
(-> ph (-> ps ch))
HIMP ph a1i
(-> ph (-> ch th))
syld
(-> ph (-> ps th))
)
edit