Theorem mulass 7917

Description: Alias for ax-mulass 7889, for naming consistency with mulassi 7941. (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 7889	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 978   = wceq 1353   e. wcel 2146  (class class class)co 5865   CCcc 7784   x. cmul 7791

This theorem was proved from axioms:  ax-mulass 7889

This theorem is referenced by:  mulid1  7929  mulassi  7941  mulassd  7955  mul12  8060  mul32  8061  mul31  8062  mul4  8063  rimul  8516  divassap  8619  cju  8889  div4p1lem1div2  9143  mulbinom2  10604  sqoddm1div8  10641  remim  10835  imval2  10869  clim2divap  11514  prod3fmul  11515  prodmodclem3  11549  absefib  11744  efieq1re  11745  muldvds1  11789  muldvds2  11790  dvdsmulc  11792  dvdstr  11801  oddprmdvds  12317  abssinper  13818  2sqlem6  14007