Theorem mulass 7623

Description: Alias for ax-mulass 7598, for naming consistency with mulassi 7647. (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 7598	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 930   = wceq 1299   e. wcel 1448  (class class class)co 5706   CCcc 7498   x. cmul 7505

This theorem was proved from axioms:  ax-mulass 7598

This theorem is referenced by:  mulid1  7635  mulassi  7647  mulassd  7661  mul12  7762  mul32  7763  mul31  7764  mul4  7765  rimul  8213  divassap  8311  cju  8577  div4p1lem1div2  8825  mulbinom2  10249  sqoddm1div8  10285  remim  10473  imval2  10507  absefib  11274  efieq1re  11275  muldvds1  11313  muldvds2  11314  dvdsmulc  11316  dvdstr  11325