Theorem addassi 11125

Description: Associative law for addition. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
axi.3	⊢ 𝐶 ∈ ℂ

Assertion

Ref	Expression
addassi	⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))

Proof of Theorem addassi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		addass 11096	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
5	1, 2, 3, 4	mp3an 1463	1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   + caddc 11012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  mul02lem2  11293  addrid  11296  2p2e4  12258  1p2e3  12266  3p2e5  12274  3p3e6  12275  4p2e6  12276  4p3e7  12277  4p4e8  12278  5p2e7  12279  5p3e8  12280  5p4e9  12281  6p2e8  12282  6p3e9  12283  7p2e9  12284  numsuc  12605  nummac  12636  numaddc  12639  6p5lem  12661  5p5e10  12662  6p4e10  12663  7p3e10  12666  8p2e10  12671  binom2i  14119  faclbnd4lem1  14200  3dvdsdec  16243  3dvds2dec  16244  gcdaddmlem  16435  mod2xnegi  16983  decsplit  16994  lgsdir2lem2  27235  2lgsoddprmlem3d  27322  ax5seglem7  28880  normlem3  31056  stadd3i  32192  dfdec100  32776  dp3mul10  32839  dpmul  32854  dpmul4  32855  cos9thpiminplylem4  33758  quad3  35653  addassnni  41967  1p3e4  42242  sn-1ne2  42248  sqmid3api  42266  re1m1e0m0  42380  sn-0tie0  42434  fltnltalem  42645  unitadd  44178  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  3exp4mod41  47610  bgoldbtbndlem1  47799