expdimp Show Code edit
## Export & Import
thm (expdimp () (exp3a.1 (-> ph (-> (/\ ps ch) th))) (-> (/\ ph ps) (-> ch th)) exp3a.1 exp3a imp)
(-> (/\ ph ps) (-> ch th))
edit