3impb Show Code edit
# Importation from double to triple conjunction.
thm (3impb () (3impb.1 (-> (/\ ph (/\ ps ch)) th)) (-> (/\/\ ph ps ch) th) 3impb.1 exp32 3imp)
(-> (/\/\ ph ps ch) th)
edit