imp Show Code edit
# Importation inference. (The proof was shortened by Eric Schmidt,
# 22-Dec-2006.)
## Import Theorem
thm (imp () (imp.1 (-> ph (-> ps ch))) (-> (/\ ph ps) ch) imp.1 ph ps ch impexp mpbir)
(-> (/\ ph ps) ch)
edit