Theorem addassi 11150

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7362  ℂcc 11031   + caddc 11036

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

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

This theorem is referenced by:  mul02lem2  11318  addrid  11321  2p2e4  12306  1p2e3  12314  3p2e5  12322  3p3e6  12323  4p2e6  12324  4p3e7  12325  4p4e8  12326  5p2e7  12327  5p3e8  12328  5p4e9  12329  6p2e8  12330  6p3e9  12331  7p2e9  12332  numsuc  12653  nummac  12684  numaddc  12687  6p5lem  12709  5p5e10  12710  6p4e10  12711  7p3e10  12714  8p2e10  12719  binom2i  14169  faclbnd4lem1  14250  3dvdsdec  16296  3dvds2dec  16297  gcdaddmlem  16488  mod2xnegi  17037  decsplit  17048  lgsdir2lem2  27307  2lgsoddprmlem3d  27394  ax5seglem7  29022  normlem3  31202  stadd3i  32338  dfdec100  32922  dp3mul10  32976  dpmul  32991  dpmul4  32992  cos9thpiminplylem4  33949  quad3  35872  addassnni  42441  1p3e4  42715  sn-1ne2  42721  sqmid3api  42733  re1m1e0m0  42847  sn-0tie0  42914  fltnltalem  43113  unitadd  44644  sqwvfoura  46678  sqwvfourb  46679  fouriersw  46681  3exp4mod41  48095  bgoldbtbndlem1  48297