3expia Show Code edit
# Exportation from triple conjunction.
thm (3expia () (3exp.1 (-> (/\/\ ph ps ch) th)) (-> (/\ ph ps) (-> ch th)) 3exp.1 3exp imp)
(-> (/\ ph ps) (-> ch th))
edit