Theorem mulass 7012

Description: Alias for ax-mulass 6987, for naming consistency with mulassi 7036. (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 6987	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 885   = wceq 1243   e. wcel 1393  (class class class)co 5512   CCcc 6887   x. cmul 6894

This theorem was proved from axioms:  ax-mulass 6987

This theorem is referenced by:  mulid1  7024  mulassi  7036  mulassd  7050  mul12  7142  mul32  7143  mul31  7144  mul4  7145  rimul  7576  divassap  7669  cju  7913  div4p1lem1div2  8177  remim  9460  imval2  9494