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