Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ax-addass | Structured version Visualization version GIF version |
Description: Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by Theorem axaddass 10896. Proofs should normally use addass 10942 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
ax-addass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . . 4 class 𝐴 | |
2 | cc 10853 | . . . 4 class ℂ | |
3 | 1, 2 | wcel 2109 | . . 3 wff 𝐴 ∈ ℂ |
4 | cB | . . . 4 class 𝐵 | |
5 | 4, 2 | wcel 2109 | . . 3 wff 𝐵 ∈ ℂ |
6 | cC | . . . 4 class 𝐶 | |
7 | 6, 2 | wcel 2109 | . . 3 wff 𝐶 ∈ ℂ |
8 | 3, 5, 7 | w3a 1085 | . 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) |
9 | caddc 10858 | . . . . 5 class + | |
10 | 1, 4, 9 | co 7268 | . . . 4 class (𝐴 + 𝐵) |
11 | 10, 6, 9 | co 7268 | . . 3 class ((𝐴 + 𝐵) + 𝐶) |
12 | 4, 6, 9 | co 7268 | . . . 4 class (𝐵 + 𝐶) |
13 | 1, 12, 9 | co 7268 | . . 3 class (𝐴 + (𝐵 + 𝐶)) |
14 | 11, 13 | wceq 1541 | . 2 wff ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
15 | 8, 14 | wi 4 | 1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Colors of variables: wff setvar class |
This axiom is referenced by: addass 10942 |
Copyright terms: Public domain | W3C validator |