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