syl5ib Show Code edit
## Syllogism
thm (syl5ib () (HIMP (-> ph (-> ps ch)) HEQ (<-> th ps)) (-> ph (-> th ch))
HIMP
(-> ph (-> ps ch))
HEQ ch imbi1i ph imbi2i biimpri
(-> (-> ph (-> ps ch)) (-> ph (-> th ch)))
ax-mp
(-> ph (-> th ch))
)
edit