![]() |
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 11235 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1458 | 1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∈ wcel 2099 (class class class)co 7415 ℂcc 11146 + caddc 11151 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addass 11213 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 |
This theorem is referenced by: mul02lem2 11431 addrid 11434 2p2e4 12392 1p2e3 12400 3p2e5 12408 3p3e6 12409 4p2e6 12410 4p3e7 12411 4p4e8 12412 5p2e7 12413 5p3e8 12414 5p4e9 12415 6p2e8 12416 6p3e9 12417 7p2e9 12418 numsuc 12736 nummac 12767 numaddc 12770 6p5lem 12792 5p5e10 12793 6p4e10 12794 7p3e10 12797 8p2e10 12802 binom2i 14223 faclbnd4lem1 14304 3dvdsdec 16328 3dvds2dec 16329 gcdaddmlem 16518 mod2xnegi 17067 decexp2 17071 decsplit 17079 lgsdir2lem2 27351 2lgsoddprmlem3d 27438 ax5seglem7 28865 normlem3 31041 stadd3i 32177 dfdec100 32733 dp3mul10 32761 dpmul 32776 dpmul4 32777 quad3 35510 addassnni 41695 sn-1ne2 42003 sqmid3api 42021 re1m1e0m0 42107 sn-0tie0 42149 fltnltalem 42351 unitadd 43898 sqwvfoura 45884 sqwvfourb 45885 fouriersw 45887 3exp4mod41 47223 bgoldbtbndlem1 47412 |
Copyright terms: Public domain | W3C validator |