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