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