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