ex Show Code edit
## Export Inference
thm (ex () (exp.1 (-> (/\ ph ps) ch)) (-> ph (-> ps ch)) exp.1 ph ps ch impexp mpbi)
(-> ph (-> ps ch))
edit