Theorem mulass 8310

Description: Alias for ax-mulass 8282, for naming consistency with mulassi 8335. (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 8282	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8177   x. cmul 8184

This proof depends on axioms:  ax-mulass 8282

This theorem is used by:  mulrid  8323  mulassi  8335  mulassd  8349  mul12  8456  mul32  8457  mul31  8458  mul4  8459  rimul  8915  divassap  9022  cju  9293  div4p1lem1div2  9563  mulbinom2  11106  sqoddm1div8  11144  remim  11639  imval2  11673  clim2divap  12323  prod3fmul  12324  prodmodclem3  12358  absefib  12554  efieq1re  12555  muldvds1  12599  muldvds2  12600  dvdsmulc  12602  dvdstr  12611  oddprmdvds  13153  cncrng  14955  abssinper  15997  pellexlem2  16149  2sqlem6  16337