3imp Show Code edit
# Importation inference.
thm (3imp () (3imp.1 (-> ph (-> ps (-> ch th)))) (-> (/\/\ ph ps ch) th) ph ps ch df-3an 3imp.1 imp31 sylbi)
(-> (/\/\ ph ps ch) th)
edit