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