Theorem mulass 8260

Description: Alias for ax-mulass 8232, for naming consistency with mulassi 8285. (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 8232	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 1005   = wceq 1398   e. wcel 2205  (class class class)co 6052   CCcc 8127   x. cmul 8134

This theorem was proved from axioms:  ax-mulass 8232

This theorem is referenced by:  mulrid  8273  mulassi  8285  mulassd  8299  mul12  8404  mul32  8405  mul31  8406  mul4  8407  rimul  8861  divassap  8966  cju  9237  div4p1lem1div2  9494  mulbinom2  11022  sqoddm1div8  11059  remim  11549  imval2  11583  clim2divap  12230  prod3fmul  12231  prodmodclem3  12265  absefib  12461  efieq1re  12462  muldvds1  12506  muldvds2  12507  dvdsmulc  12509  dvdstr  12518  oddprmdvds  13056  cncrng  14734  abssinper  15728  pellexlem2  15863  2sqlem6  16010