imp31 Show Code edit
## Import Inference
thm (imp31 () (imp3.1 (-> ph (-> ps (-> ch th)))) (-> (/\ (/\ ph ps) ch) th) imp3.1 imp imp)
(-> (/\ (/\ ph ps) ch) th)
edit