Theorem mulass 8058

Description: Alias for ax-mulass 8030, for naming consistency with mulassi 8083. (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 8030	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 981   = wceq 1373   e. wcel 2176  (class class class)co 5946   CCcc 7925   x. cmul 7932

This theorem was proved from axioms:  ax-mulass 8030

This theorem is referenced by:  mulrid  8071  mulassi  8083  mulassd  8098  mul12  8203  mul32  8204  mul31  8205  mul4  8206  rimul  8660  divassap  8765  cju  9036  div4p1lem1div2  9293  mulbinom2  10803  sqoddm1div8  10840  remim  11204  imval2  11238  clim2divap  11884  prod3fmul  11885  prodmodclem3  11919  absefib  12115  efieq1re  12116  muldvds1  12160  muldvds2  12161  dvdsmulc  12163  dvdstr  12172  oddprmdvds  12710  cncrng  14364  abssinper  15351  2sqlem6  15630