Theorem mulass 8056

Description: Alias for ax-mulass 8028, for naming consistency with mulassi 8081. (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 8028	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 2176  (class class class)co 5944   CCcc 7923   x. cmul 7930

This theorem was proved from axioms:  ax-mulass 8028

This theorem is referenced by:  mulrid  8069  mulassi  8081  mulassd  8096  mul12  8201  mul32  8202  mul31  8203  mul4  8204  rimul  8658  divassap  8763  cju  9034  div4p1lem1div2  9291  mulbinom2  10801  sqoddm1div8  10838  remim  11171  imval2  11205  clim2divap  11851  prod3fmul  11852  prodmodclem3  11886  absefib  12082  efieq1re  12083  muldvds1  12127  muldvds2  12128  dvdsmulc  12130  dvdstr  12139  oddprmdvds  12677  cncrng  14331  abssinper  15318  2sqlem6  15597