himp1i Show Code edit
##
## (-> (-> ph [ ps ] ) [ ch)
## (-> [ ps ] [ ch)
##
thm (himp1i () (1 (-> (-> ph ps) ch)) (-> ps ch)
ps ph ax-1 1 syl)
(-> ps ch)
edit