Theorem mulassi 8342

Description: Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	|- A e. CC
axi.2	|- B e. CC
axi.3	|- C e. CC

Assertion

Ref	Expression
mulassi	|- ( ( A x. B ) x. C ) = ( A x. ( B x. C ) )

Proof of Theorem mulassi

Step	Hyp	Ref	Expression
1		axi.1	. 2 |- A e. CC
2		axi.2	. 2 |- B e. CC
3		axi.3	. 2 |- C e. CC
4		mulass 8317	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
5	1, 2, 3, 4	mp3an 1378	1 |- ( ( A x. B ) x. C ) = ( A x. ( B x. C ) )

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209  (class class class)co 6088   CCcc 8184   x. cmul 8191

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-mulass 8289

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  8th4div3  9536  numma  9836  decbin0  9932  sq4e2t8  11095  3dec  11174  ef01bndlem  12548  3dvdsdec  12657  3dvds2dec  12658  dec5dvds  13220  karatsuba  13239  sincos4thpi  16100  sincos6thpi  16102  log2ublem2  16255  log2ublem3  16256  log2ublog2  16257  bclbnd  16340  bposlem8  16351  2lgsoddprmlem3d  16467