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 10612 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1452 | 1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 + caddc 10528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addass 10590 |
This theorem depends on definitions: df-bi 208 df-an 397 df-3an 1081 |
This theorem is referenced by: mul02lem2 10805 addid1 10808 2p2e4 11760 1p2e3 11768 3p2e5 11776 3p3e6 11777 4p2e6 11778 4p3e7 11779 4p4e8 11780 5p2e7 11781 5p3e8 11782 5p4e9 11783 6p2e8 11784 6p3e9 11785 7p2e9 11786 numsuc 12100 nummac 12131 numaddc 12134 6p5lem 12156 5p5e10 12157 6p4e10 12158 7p3e10 12161 8p2e10 12166 binom2i 13562 faclbnd4lem1 13641 3dvdsdec 15669 3dvds2dec 15670 gcdaddmlem 15860 mod2xnegi 16395 decexp2 16399 decsplit 16407 lgsdir2lem2 25829 2lgsoddprmlem3d 25916 ax5seglem7 26648 normlem3 28816 stadd3i 29952 dfdec100 30473 dp3mul10 30501 dpmul 30516 dpmul4 30517 quad3 32810 sn-1ne2 39036 sqmid3api 39047 re1m1e0m0 39105 fltnltalem 39152 unitadd 40426 sqwvfoura 42390 sqwvfourb 42391 fouriersw 42393 3exp4mod41 43658 bgoldbtbndlem1 43847 |
Copyright terms: Public domain | W3C validator |