3anass Show Code edit
# Associative law for triple conjunction.
thm (3anass () () (<-> (/\/\ ph ps ch) (/\ ph (/\ ps ch))) ph ps ch df-3an ph ps ch anass bitri)
(<-> (/\/\ ph ps ch) (/\ ph (/\ ps ch)))
edit