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