Theorem addassi 11146

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028   + caddc 11033

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

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

This theorem is referenced by:  mul02lem2  11314  addrid  11317  2p2e4  12279  1p2e3  12287  3p2e5  12295  3p3e6  12296  4p2e6  12297  4p3e7  12298  4p4e8  12299  5p2e7  12300  5p3e8  12301  5p4e9  12302  6p2e8  12303  6p3e9  12304  7p2e9  12305  numsuc  12625  nummac  12656  numaddc  12659  6p5lem  12681  5p5e10  12682  6p4e10  12683  7p3e10  12686  8p2e10  12691  binom2i  14139  faclbnd4lem1  14220  3dvdsdec  16263  3dvds2dec  16264  gcdaddmlem  16455  mod2xnegi  17003  decsplit  17014  lgsdir2lem2  27297  2lgsoddprmlem3d  27384  ax5seglem7  29012  normlem3  31191  stadd3i  32327  dfdec100  32913  dp3mul10  32981  dpmul  32996  dpmul4  32997  cos9thpiminplylem4  33944  quad3  35866  addassnni  42306  1p3e4  42581  sn-1ne2  42587  sqmid3api  42605  re1m1e0m0  42719  sn-0tie0  42773  fltnltalem  42972  unitadd  44503  sqwvfoura  46539  sqwvfourb  46540  fouriersw  46542  3exp4mod41  47929  bgoldbtbndlem1  48118