Theorem mulass 8223

Description: Alias for ax-mulass 8195, for naming consistency with mulassi 8248. (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 8195	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 1005   = wceq 1398   e. wcel 2202  (class class class)co 6028   CCcc 8090   x. cmul 8097

This theorem was proved from axioms:  ax-mulass 8195

This theorem is referenced by:  mulrid  8236  mulassi  8248  mulassd  8262  mul12  8367  mul32  8368  mul31  8369  mul4  8370  rimul  8824  divassap  8929  cju  9200  div4p1lem1div2  9457  mulbinom2  10981  sqoddm1div8  11018  remim  11500  imval2  11534  clim2divap  12181  prod3fmul  12182  prodmodclem3  12216  absefib  12412  efieq1re  12413  muldvds1  12457  muldvds2  12458  dvdsmulc  12460  dvdstr  12469  oddprmdvds  13007  cncrng  14665  abssinper  15657  pellexlem2  15792  2sqlem6  15939