Theorem addassi 11140

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022   + caddc 11027

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

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

This theorem is referenced by:  mul02lem2  11308  addrid  11311  2p2e4  12273  1p2e3  12281  3p2e5  12289  3p3e6  12290  4p2e6  12291  4p3e7  12292  4p4e8  12293  5p2e7  12294  5p3e8  12295  5p4e9  12296  6p2e8  12297  6p3e9  12298  7p2e9  12299  numsuc  12619  nummac  12650  numaddc  12653  6p5lem  12675  5p5e10  12676  6p4e10  12677  7p3e10  12680  8p2e10  12685  binom2i  14133  faclbnd4lem1  14214  3dvdsdec  16257  3dvds2dec  16258  gcdaddmlem  16449  mod2xnegi  16997  decsplit  17008  lgsdir2lem2  27291  2lgsoddprmlem3d  27378  ax5seglem7  28957  normlem3  31136  stadd3i  32272  dfdec100  32860  dp3mul10  32928  dpmul  32943  dpmul4  32944  cos9thpiminplylem4  33891  quad3  35813  addassnni  42177  1p3e4  42456  sn-1ne2  42462  sqmid3api  42480  re1m1e0m0  42594  sn-0tie0  42648  fltnltalem  42847  unitadd  44378  sqwvfoura  46414  sqwvfourb  46415  fouriersw  46417  3exp4mod41  47804  bgoldbtbndlem1  47993