Axiom ax-mulass

Description: Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by Theorem axmulass . Proofs should normally use mulass instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

	Ref	Expression
Assertion	ax-mulass	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cc	|- CC
2	0 1	wcel	|- A e. CC
3		cB	|- B
4	3 1	wcel	|- B e. CC
5		cC	|- C
6	5 1	wcel	|- C e. CC
7	2 4 6	w3a	|- ( A e. CC /\ B e. CC /\ C e. CC )
8		cmul	|- x.
9	0 3 8	co	|- ( A x. B )
10	9 5 8	co	|- ( ( A x. B ) x. C )
11	3 5 8	co	|- ( B x. C )
12	0 11 8	co	|- ( A x. ( B x. C ) )
13	10 12	wceq	|- ( ( A x. B ) x. C ) = ( A x. ( B x. C ) )
14	7 13	wi	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )