Theorem mulass 7884

Description: Alias for ax-mulass 7856, for naming consistency with mulassi 7908. (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 7856	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 968   = wceq 1343   e. wcel 2136  (class class class)co 5842   CCcc 7751   x. cmul 7758

This theorem was proved from axioms:  ax-mulass 7856

This theorem is referenced by:  mulid1  7896  mulassi  7908  mulassd  7922  mul12  8027  mul32  8028  mul31  8029  mul4  8030  rimul  8483  divassap  8586  cju  8856  div4p1lem1div2  9110  mulbinom2  10571  sqoddm1div8  10608  remim  10802  imval2  10836  clim2divap  11481  prod3fmul  11482  prodmodclem3  11516  absefib  11711  efieq1re  11712  muldvds1  11756  muldvds2  11757  dvdsmulc  11759  dvdstr  11768  oddprmdvds  12284  abssinper  13407  2sqlem6  13596