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