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