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	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to ABC=ABC$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cc	$$classℂ$$
2	0 1	wcel	$$wffA\in ℂ$$
3		cB	$$classB$$
4	3 1	wcel	$$wffB\in ℂ$$
5		cC	$$classC$$
6	5 1	wcel	$$wffC\in ℂ$$
7	2 4 6	w3a	$$wff\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)$$
8		cmul	$$class\times$$
9	0 3 8	co	$$classAB$$
10	9 5 8	co	$$classABC$$
11	3 5 8	co	$$classBC$$
12	0 11 8	co	$$classABC$$
13	10 12	wceq	$$wffABC=ABC$$
14	7 13	wi	$$wff\left(\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to ABC=ABC\right)$$