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