3exp1 Show Code edit
# Exportation from left triple conjunction.
thm (3exp1 () (3exp1.1 (-> (/\ (/\/\ ph ps ch) th) ta)) (-> ph (-> ps (-> ch (-> th ta)))) 3exp1.1 ex 3exp)
(-> ph (-> ps (-> ch (-> th ta))))
edit