Theorem mulass 8091

Description: Alias for ax-mulass 8063, for naming consistency with mulassi 8116. (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 8063	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 981   = wceq 1373   e. wcel 2178  (class class class)co 5967   CCcc 7958   x. cmul 7965

This theorem was proved from axioms:  ax-mulass 8063

This theorem is referenced by:  mulrid  8104  mulassi  8116  mulassd  8131  mul12  8236  mul32  8237  mul31  8238  mul4  8239  rimul  8693  divassap  8798  cju  9069  div4p1lem1div2  9326  mulbinom2  10838  sqoddm1div8  10875  remim  11286  imval2  11320  clim2divap  11966  prod3fmul  11967  prodmodclem3  12001  absefib  12197  efieq1re  12198  muldvds1  12242  muldvds2  12243  dvdsmulc  12245  dvdstr  12254  oddprmdvds  12792  cncrng  14446  abssinper  15433  2sqlem6  15712