3impia Show Code edit
# Importation to triple conjunction.
thm (3impia () (3impia.1 (-> (/\ ph ps) (-> ch th))) (-> (/\/\ ph ps ch) th) 3impia.1 ex 3imp)
(-> (/\/\ ph ps ch) th)
edit