![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > addassi | Structured version Visualization version 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 10359 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1534 | 1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 ∈ wcel 2107 (class class class)co 6922 ℂcc 10270 + caddc 10275 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addass 10337 |
This theorem depends on definitions: df-bi 199 df-an 387 df-3an 1073 |
This theorem is referenced by: mul02lem2 10553 addid1 10556 2p2e4 11517 1p2e3 11525 3p2e5 11533 3p3e6 11534 4p2e6 11535 4p3e7 11536 4p4e8 11537 5p2e7 11538 5p3e8 11539 5p4e9 11540 6p2e8 11541 6p3e9 11542 7p2e9 11543 numsuc 11859 nummac 11891 numaddc 11894 6p5lem 11917 5p5e10 11918 6p4e10 11919 7p3e10 11922 8p2e10 11927 binom2i 13293 faclbnd4lem1 13398 3dvdsdec 15460 3dvds2dec 15461 gcdaddmlem 15651 mod2xnegi 16179 decexp2 16183 decsplit 16191 lgsdir2lem2 25503 2lgsoddprmlem3d 25590 ax5seglem7 26284 normlem3 28541 stadd3i 29679 dfdec100 30140 dp3mul10 30168 dpmul 30183 dpmul4 30184 quad3 32161 sqmid3api 38149 unitadd 39454 sqwvfoura 41372 sqwvfourb 41373 fouriersw 41375 3exp4mod41 42554 bgoldbtbndlem1 42718 |
Copyright terms: Public domain | W3C validator |