![]() |
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 11273 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1461 | 1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ∈ wcel 2108 (class class class)co 7450 ℂcc 11184 + caddc 11189 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addass 11251 |
This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 |
This theorem is referenced by: mul02lem2 11469 addrid 11472 2p2e4 12430 1p2e3 12438 3p2e5 12446 3p3e6 12447 4p2e6 12448 4p3e7 12449 4p4e8 12450 5p2e7 12451 5p3e8 12452 5p4e9 12453 6p2e8 12454 6p3e9 12455 7p2e9 12456 numsuc 12774 nummac 12805 numaddc 12808 6p5lem 12830 5p5e10 12831 6p4e10 12832 7p3e10 12835 8p2e10 12840 binom2i 14263 faclbnd4lem1 14344 3dvdsdec 16382 3dvds2dec 16383 gcdaddmlem 16572 mod2xnegi 17120 decexp2 17124 decsplit 17132 lgsdir2lem2 27390 2lgsoddprmlem3d 27477 ax5seglem7 28970 normlem3 31146 stadd3i 32282 dfdec100 32836 dp3mul10 32864 dpmul 32879 dpmul4 32880 quad3 35640 addassnni 41943 sn-1ne2 42256 sqmid3api 42274 re1m1e0m0 42375 sn-0tie0 42417 fltnltalem 42619 unitadd 44159 sqwvfoura 46151 sqwvfourb 46152 fouriersw 46154 3exp4mod41 47492 bgoldbtbndlem1 47681 |
Copyright terms: Public domain | W3C validator |