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