3expd Show Code edit
# Exportation deduction for triple conjunction.
thm (3expd () (3expd.1 (-> ph (-> (/\/\ ps ch th) ta))) (-> ph (-> ps (-> ch (-> th ta)))) 3expd.1 com12 3exp com4r)
(-> ph (-> ps (-> ch (-> th ta))))
edit