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 7904 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1332 | 1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Colors of variables: wff set class |
Syntax hints: = wceq 1348 ∈ wcel 2141 (class class class)co 5853 ℂcc 7772 + caddc 7777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-addass 7876 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: 2p2e4 9005 3p2e5 9019 3p3e6 9020 4p2e6 9021 4p3e7 9022 4p4e8 9023 5p2e7 9024 5p3e8 9025 5p4e9 9026 6p2e8 9027 6p3e9 9028 7p2e9 9029 numsuc 9356 nummac 9387 numaddc 9390 6p5lem 9412 5p5e10 9413 6p4e10 9414 7p3e10 9417 8p2e10 9422 binom2i 10584 resqrexlemover 10974 3dvdsdec 11824 3dvds2dec 11825 lgsdir2lem2 13724 |
Copyright terms: Public domain | W3C validator |