Metamath Proof Explorer


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 ABCA+B+C=A+B+C

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA classA
1 cc class
2 0 1 wcel wffA
3 cB classB
4 3 1 wcel wffB
5 cC classC
6 5 1 wcel wffC
7 2 4 6 w3a wffABC
8 caddc class+
9 0 3 8 co classA+B
10 9 5 8 co classA+B+C
11 3 5 8 co classB+C
12 0 11 8 co classA+B+C
13 10 12 wceq wffA+B+C=A+B+C
14 7 13 wi wffABCA+B+C=A+B+C