Theorem addassi 11228

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

Syntax hints:   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   + caddc 11115

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087

This theorem is referenced by:  mul02lem2  11395  addrid  11398  2p2e4  12351  1p2e3  12359  3p2e5  12367  3p3e6  12368  4p2e6  12369  4p3e7  12370  4p4e8  12371  5p2e7  12372  5p3e8  12373  5p4e9  12374  6p2e8  12375  6p3e9  12376  7p2e9  12377  numsuc  12695  nummac  12726  numaddc  12729  6p5lem  12751  5p5e10  12752  6p4e10  12753  7p3e10  12756  8p2e10  12761  binom2i  14180  faclbnd4lem1  14257  3dvdsdec  16279  3dvds2dec  16280  gcdaddmlem  16469  mod2xnegi  17008  decexp2  17012  decsplit  17020  lgsdir2lem2  27065  2lgsoddprmlem3d  27152  ax5seglem7  28460  normlem3  30632  stadd3i  31768  dfdec100  32303  dp3mul10  32331  dpmul  32346  dpmul4  32347  quad3  34953  addassnni  41156  sn-1ne2  41481  sqmid3api  41497  re1m1e0m0  41572  sn-0tie0  41614  fltnltalem  41706  unitadd  43249  sqwvfoura  45242  sqwvfourb  45243  fouriersw  45245  3exp4mod41  46582  bgoldbtbndlem1  46771