3impib Show Code edit
# Importation to triple conjunction.
thm (3impib () (3impib.1 (-> ph (-> (/\ ps ch) th))) (-> (/\/\ ph ps ch) th) 3impib.1 exp3a 3imp)
(-> (/\/\ ph ps ch) th)
edit