3expa Show Code edit
# Exportation from triple to double conjunction.
thm (3expa () (3exp.1 (-> (/\/\ ph ps ch) th)) (-> (/\ (/\ ph ps) ch) th) 3exp.1 3exp imp31)
(-> (/\ (/\ ph ps) ch) th)
edit