Theorem addassi 11219

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 11187	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
5	1, 2, 3, 4	mp3an 1487	1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))

Syntax hints:   = wceq 1567   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098   + caddc 11103

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103

This theorem is referenced by:  mul02lem2  11387  addrid  11390  2p2e4  12375  1p2e3  12383  3p2e5  12391  3p3e6  12392  4p2e6  12393  4p3e7  12394  4p4e8  12395  5p2e7  12396  5p3e8  12397  5p4e9  12398  6p2e8  12399  6p3e9  12400  7p2e9  12401  numsuc  12725  nummac  12761  numaddc  12764  6p5lem  12786  5p5e10  12787  6p4e10  12788  7p3e10  12791  8p2e10  12796  binom2i  14248  faclbnd4lem1  14329  3dvdsdec  16390  3dvds2dec  16391  gcdaddmlem  16582  mod2xnegi  17131  decsplit  17142  lgsdir2lem2  27456  2lgsoddprmlem3d  27543  ax5seglem7  29226  normlem3  31405  stadd3i  32541  dfdec100  33115  dp3mul10  33158  dpmul  33173  dpmul4  33174  cos9thpiminplylem4  34120  quad3  36095  addassnni  42675  1p3e4  42950  sn-1ne2  42956  sqmid3api  42968  re1m1e0m0  43082  sn-0tie0  43149  fltnltalem  43320  unitadd  44847  sqwvfoura  46868  sqwvfourb  46869  fouriersw  46871  3exp4mod41  48291  bgoldbtbndlem1  48493