anass Show Code edit
# Associative law for conjunction. Theorem *4.32 of [bib/WhiteheadRussell]
# p. 118.
## Associative Property
## right('Associate', 'R') left('Associate', 'L')
thm (anass () () (<-> (/\ (/\ ph ps) ch) (/\ ph (/\ ps ch))) ph ps (-. ch) impexp ps ch imnan ph imbi2i bitri notbii (/\ ph ps) ch df-an ph (/\ ps ch) df-an 3bitr4i)
(<-> (/\ (/\ ph ps) ch) (/\ ph (/\ ps ch)))
edit