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