syl7ib Show Code edit
## Syllogism
thm (syl7ib () (HIMP (-> ph (-> ps (-> ch th))) HEQ (<-> ta ch)) (-> ph (-> ps (-> ta th)))
HIMP
(-> ph (-> ps (-> ch th)))
HEQ biimpi
(-> ta ch)
syl7
(-> ph (-> ps (-> ta th)))
)
edit