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