Theorem mulass 8163

Description: Alias for ax-mulass 8135, for naming consistency with mulassi 8188. (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 8135	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 1004   = wceq 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   x. cmul 8037

This theorem was proved from axioms:  ax-mulass 8135

This theorem is referenced by:  mulrid  8176  mulassi  8188  mulassd  8203  mul12  8308  mul32  8309  mul31  8310  mul4  8311  rimul  8765  divassap  8870  cju  9141  div4p1lem1div2  9398  mulbinom2  10919  sqoddm1div8  10956  remim  11438  imval2  11472  clim2divap  12119  prod3fmul  12120  prodmodclem3  12154  absefib  12350  efieq1re  12351  muldvds1  12395  muldvds2  12396  dvdsmulc  12398  dvdstr  12407  oddprmdvds  12945  cncrng  14602  abssinper  15589  2sqlem6  15868