Theorem mulass 7751

Description: Alias for ax-mulass 7723, for naming consistency with mulassi 7775. (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 7723	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 962   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   x. cmul 7625

This theorem was proved from axioms:  ax-mulass 7723

This theorem is referenced by:  mulid1  7763  mulassi  7775  mulassd  7789  mul12  7891  mul32  7892  mul31  7893  mul4  7894  rimul  8347  divassap  8450  cju  8719  div4p1lem1div2  8973  mulbinom2  10408  sqoddm1div8  10444  remim  10632  imval2  10666  clim2divap  11309  prod3fmul  11310  prodmodclem3  11344  absefib  11477  efieq1re  11478  muldvds1  11518  muldvds2  11519  dvdsmulc  11521  dvdstr  11530  abssinper  12927