3impa Show Code edit
# Importation from double to triple conjunction.
thm (3impa () (3impa.1 (-> (/\ (/\ ph ps) ch) th)) (-> (/\/\ ph ps ch) th) 3impa.1 exp31 3imp)
(-> (/\/\ ph ps ch) th)
edit