![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addassi | GIF version |
Description: Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
axi.2 | ⊢ 𝐵 ∈ ℂ |
axi.3 | ⊢ 𝐶 ∈ ℂ |
Ref | Expression |
---|---|
addassi | ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | axi.2 | . 2 ⊢ 𝐵 ∈ ℂ | |
3 | axi.3 | . 2 ⊢ 𝐶 ∈ ℂ | |
4 | addass 7940 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1337 | 1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Colors of variables: wff set class |
Syntax hints: = wceq 1353 ∈ wcel 2148 (class class class)co 5874 ℂcc 7808 + caddc 7813 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-addass 7912 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 2p2e4 9044 3p2e5 9058 3p3e6 9059 4p2e6 9060 4p3e7 9061 4p4e8 9062 5p2e7 9063 5p3e8 9064 5p4e9 9065 6p2e8 9066 6p3e9 9067 7p2e9 9068 numsuc 9395 nummac 9426 numaddc 9429 6p5lem 9451 5p5e10 9452 6p4e10 9453 7p3e10 9456 8p2e10 9461 binom2i 10625 resqrexlemover 11014 3dvdsdec 11864 3dvds2dec 11865 lgsdir2lem2 14361 |
Copyright terms: Public domain | W3C validator |