Theorem mulass 8130

Description: Alias for ax-mulass 8102, for naming consistency with mulassi 8155. (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 8102	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 1002   = wceq 1395   e. wcel 2200  (class class class)co 6001   CCcc 7997   x. cmul 8004

This theorem was proved from axioms:  ax-mulass 8102

This theorem is referenced by:  mulrid  8143  mulassi  8155  mulassd  8170  mul12  8275  mul32  8276  mul31  8277  mul4  8278  rimul  8732  divassap  8837  cju  9108  div4p1lem1div2  9365  mulbinom2  10878  sqoddm1div8  10915  remim  11371  imval2  11405  clim2divap  12051  prod3fmul  12052  prodmodclem3  12086  absefib  12282  efieq1re  12283  muldvds1  12327  muldvds2  12328  dvdsmulc  12330  dvdstr  12339  oddprmdvds  12877  cncrng  14533  abssinper  15520  2sqlem6  15799