exp3a Show Code edit
## Export Deduction
thm (exp3a () (exp3a.1 (-> ph (-> (/\ ps ch) th))) (-> ph (-> ps (-> ch th))) exp3a.1 ps ch th impexp sylib)
(-> ph (-> ps (-> ch th)))
edit