Theorem addassi 11128

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  (class class class)co 7352  ℂcc 11010   + caddc 11015

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

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

This theorem is referenced by:  mul02lem2  11296  addrid  11299  2p2e4  12261  1p2e3  12269  3p2e5  12277  3p3e6  12278  4p2e6  12279  4p3e7  12280  4p4e8  12281  5p2e7  12282  5p3e8  12283  5p4e9  12284  6p2e8  12285  6p3e9  12286  7p2e9  12287  numsuc  12608  nummac  12639  numaddc  12642  6p5lem  12664  5p5e10  12665  6p4e10  12666  7p3e10  12669  8p2e10  12674  binom2i  14125  faclbnd4lem1  14206  3dvdsdec  16249  3dvds2dec  16250  gcdaddmlem  16441  mod2xnegi  16989  decsplit  17000  lgsdir2lem2  27270  2lgsoddprmlem3d  27357  ax5seglem7  28920  normlem3  31099  stadd3i  32235  dfdec100  32820  dp3mul10  32885  dpmul  32900  dpmul4  32901  cos9thpiminplylem4  33805  quad3  35721  addassnni  42083  1p3e4  42358  sn-1ne2  42364  sqmid3api  42382  re1m1e0m0  42496  sn-0tie0  42550  fltnltalem  42761  unitadd  44293  sqwvfoura  46331  sqwvfourb  46332  fouriersw  46334  3exp4mod41  47721  bgoldbtbndlem1  47910