Theorem addassi 11160

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   + caddc 11047

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

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

This theorem is referenced by:  mul02lem2  11327  addrid  11330  2p2e4  12292  1p2e3  12300  3p2e5  12308  3p3e6  12309  4p2e6  12310  4p3e7  12311  4p4e8  12312  5p2e7  12313  5p3e8  12314  5p4e9  12315  6p2e8  12316  6p3e9  12317  7p2e9  12318  numsuc  12639  nummac  12670  numaddc  12673  6p5lem  12695  5p5e10  12696  6p4e10  12697  7p3e10  12700  8p2e10  12705  binom2i  14153  faclbnd4lem1  14234  3dvdsdec  16278  3dvds2dec  16279  gcdaddmlem  16470  mod2xnegi  17018  decsplit  17029  lgsdir2lem2  27270  2lgsoddprmlem3d  27357  ax5seglem7  28915  normlem3  31091  stadd3i  32227  dfdec100  32805  dp3mul10  32868  dpmul  32883  dpmul4  32884  cos9thpiminplylem4  33768  quad3  35650  addassnni  41965  1p3e4  42240  sn-1ne2  42246  sqmid3api  42264  re1m1e0m0  42378  sn-0tie0  42432  fltnltalem  42643  unitadd  44177  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  3exp4mod41  47610  bgoldbtbndlem1  47799