Theorem mulass 8027

Description: Alias for ax-mulass 7999, for naming consistency with mulassi 8052. (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 7999	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 980   = wceq 1364   e. wcel 2167  (class class class)co 5925   CCcc 7894   x. cmul 7901

This theorem was proved from axioms:  ax-mulass 7999

This theorem is referenced by:  mulrid  8040  mulassi  8052  mulassd  8067  mul12  8172  mul32  8173  mul31  8174  mul4  8175  rimul  8629  divassap  8734  cju  9005  div4p1lem1div2  9262  mulbinom2  10765  sqoddm1div8  10802  remim  11042  imval2  11076  clim2divap  11722  prod3fmul  11723  prodmodclem3  11757  absefib  11953  efieq1re  11954  muldvds1  11998  muldvds2  11999  dvdsmulc  12001  dvdstr  12010  oddprmdvds  12548  cncrng  14201  abssinper  15166  2sqlem6  15445