Axiom ax-addass

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

	Ref	Expression
Assertion	ax-addass	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to A+B+C=A+B+C$$

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		caddc	$$class+$$
9	0 3 8	co	$$class\left(A+B\right)$$
10	9 5 8	co	$$class\left(A+B+C\right)$$
11	3 5 8	co	$$class\left(B+C\right)$$
12	0 11 8	co	$$class\left(A+B+C\right)$$
13	10 12	wceq	$$wffA+B+C=A+B+C$$
14	7 13	wi	$$wff\left(\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to A+B+C=A+B+C\right)$$