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