Axiom ax-addass 10867

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

Assertion

Ref	Expression
ax-addass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Detailed syntax breakdown of Axiom ax-addass

Step	Hyp	Ref	Expression
1		cA	. . . 4 class 𝐴
2		cc 10800	. . . 4 class ℂ
3	1, 2	wcel 2108	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2108	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7	6, 2	wcel 2108	. . 3 wff 𝐶 ∈ ℂ
8	3, 5, 7	w3a 1085	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)
9		caddc 10805	. . . . 5 class +
10	1, 4, 9	co 7255	. . . 4 class (𝐴 + 𝐵)
11	10, 6, 9	co 7255	. . 3 class ((𝐴 + 𝐵) + 𝐶)
12	4, 6, 9	co 7255	. . . 4 class (𝐵 + 𝐶)
13	1, 12, 9	co 7255	. . 3 class (𝐴 + (𝐵 + 𝐶))
14	11, 13	wceq 1539	. 2 wff ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
15	8, 14	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

This axiom is referenced by:  addass  10889