Theorem mulass 8141

Description: Alias for ax-mulass 8113, for naming consistency with mulassi 8166. (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 8113	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 6007   CCcc 8008   x. cmul 8015

This theorem was proved from axioms:  ax-mulass 8113

This theorem is referenced by:  mulrid  8154  mulassi  8166  mulassd  8181  mul12  8286  mul32  8287  mul31  8288  mul4  8289  rimul  8743  divassap  8848  cju  9119  div4p1lem1div2  9376  mulbinom2  10890  sqoddm1div8  10927  remim  11387  imval2  11421  clim2divap  12067  prod3fmul  12068  prodmodclem3  12102  absefib  12298  efieq1re  12299  muldvds1  12343  muldvds2  12344  dvdsmulc  12346  dvdstr  12355  oddprmdvds  12893  cncrng  14549  abssinper  15536  2sqlem6  15815