Theorem addassi 11343

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  (class class class)co 7440  ℂcc 11222   + caddc 11227

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11289

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mul02lem2  11511  addrid  11514  2p2e4  12501  1p2e3  12509  3p2e5  12517  3p3e6  12518  4p2e6  12519  4p3e7  12520  4p4e8  12521  5p2e7  12522  5p3e8  12523  5p4e9  12524  6p2e8  12525  6p3e9  12526  7p2e9  12527  numsuc  12852  nummac  12888  numaddc  12891  6p5lem  12913  5p5e10  12914  6p4e10  12915  7p3e10  12918  8p2e10  12923  binom2i  14380  faclbnd4lem1  14461  3dvdsdec  16528  3dvds2dec  16529  gcdaddmlem  16722  mod2xnegi  17275  decsplit  17286  lgsdir2lem2  27680  2lgsoddprmlem3d  27767  ax5seglem7  29540  normlem3  31741  stadd3i  32877  dfdec100  33488  dp3mul10  33531  dpmul  33546  dpmul4  33547  cos9thpiminplylem4  34484  quad3  36601  addassnni  43225  4p4e8ALT  43500  1p3e4  43501  1p4e5  43502  1p5e6  43503  1p6e7  43504  1p7e8  43505  1p8e9  43506  2p3e5  43507  2p4e6  43508  2p5e7  43509  2p6e8  43510  2p7e9  43511  3p4e7  43512  3p5e8  43513  3p6e9  43514  4p5e9  43515  sn-1ne2  43521  sqmid3api  43531  re1m1e0m0  43639  sn-0tie0  43706  fltnltalem  43864  unitadd  45385  sqwvfoura  47441  sqwvfourb  47442  fouriersw  47444  goldpolyfactor  48130  3exp4mod41  48904  bgoldbtbndlem1  49106