Theorem mulass 7905

Description: Alias for ax-mulass 7877, for naming consistency with mulassi 7929. (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 7877	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 973   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   x. cmul 7779

This theorem was proved from axioms:  ax-mulass 7877

This theorem is referenced by:  mulid1  7917  mulassi  7929  mulassd  7943  mul12  8048  mul32  8049  mul31  8050  mul4  8051  rimul  8504  divassap  8607  cju  8877  div4p1lem1div2  9131  mulbinom2  10592  sqoddm1div8  10629  remim  10824  imval2  10858  clim2divap  11503  prod3fmul  11504  prodmodclem3  11538  absefib  11733  efieq1re  11734  muldvds1  11778  muldvds2  11779  dvdsmulc  11781  dvdstr  11790  oddprmdvds  12306  abssinper  13561  2sqlem6  13750