m,n,x:
. m
(nx) = (mn)x 
Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. all
Thm* (
m:hnum. (n:hnum. (p:hnum. equal(mult(m,mult(n,p)),mult(mult(m,n),p)))))| Theorem | Name |
| m,n,x:. m(nx) = (mn)x | [mult_assoc] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. all
Thm* ( m:hnum. (n:hnum. (p:hnum. equal(mult(m,mult(n,p)),mult(mult(m,n),p))))) | [hmult_assoc] |