3exp Show Code edit
# Exportation inference.
thm (3exp () (3exp.1 (-> (/\/\ ph ps ch) th)) (-> ph (-> ps (-> ch th))) ph ps ch df-3an 3exp.1 sylbir exp31)
(-> ph (-> ps (-> ch th)))
edit