Theorem mulassi 8336

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 8311	. 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 6085   CCcc 8178   x. cmul 8185

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 8283

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

This theorem is used by:  8th4div3  9529  numma  9830  decbin0  9926  sq4e2t8  11088  3dec  11167  ef01bndlem  12541  3dvdsdec  12650  3dvds2dec  12651  dec5dvds  13213  karatsuba  13232  sincos4thpi  15994  sincos6thpi  15996  log2ublem2  16144  log2ublem3  16145  log2ublog2  16146  bclbnd  16229  2lgsoddprmlem3d  16351