Theorem mulass 7104

Description: Alias for ax-mulass 7079, for naming consistency with mulassi 7128. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulass	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

Proof of Theorem mulass

Step	Hyp	Ref	Expression
1		ax-mulass 7079	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

Syntax hints:   -> wi 4   /\ w3a 919   = wceq 1284   e. wcel 1433  (class class class)co 5532   CCcc 6979   x. cmul 6986

This theorem was proved from axioms:  ax-mulass 7079

This theorem is referenced by:  mulid1  7116  mulassi  7128  mulassd  7142  mul12  7237  mul32  7238  mul31  7239  mul4  7240  rimul  7685  divassap  7778  cju  8038  div4p1lem1div2  8284  mulbinom2  9589  sqoddm1div8  9625  remim  9747  imval2  9781  muldvds1  10220  muldvds2  10221  dvdsmulc  10223  dvdstr  10232