imp3a Show Code edit
## Import Deduction
thm (imp3a () (imp3.1 (-> ph (-> ps (-> ch th)))) (-> ph (-> (/\ ps ch) th)) imp3.1 ps ch th impexp sylibr)
(-> ph (-> (/\ ps ch) th))
edit