Theorem addassi 11155

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

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

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

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

This theorem is referenced by:  mul02lem2  11323  addrid  11326  2p2e4  12311  1p2e3  12319  3p2e5  12327  3p3e6  12328  4p2e6  12329  4p3e7  12330  4p4e8  12331  5p2e7  12332  5p3e8  12333  5p4e9  12334  6p2e8  12335  6p3e9  12336  7p2e9  12337  numsuc  12658  nummac  12689  numaddc  12692  6p5lem  12714  5p5e10  12715  6p4e10  12716  7p3e10  12719  8p2e10  12724  binom2i  14174  faclbnd4lem1  14255  3dvdsdec  16301  3dvds2dec  16302  gcdaddmlem  16493  mod2xnegi  17042  decsplit  17053  lgsdir2lem2  27289  2lgsoddprmlem3d  27376  ax5seglem7  29004  normlem3  31183  stadd3i  32319  dfdec100  32903  dp3mul10  32957  dpmul  32972  dpmul4  32973  cos9thpiminplylem4  33929  quad3  35852  addassnni  42423  1p3e4  42697  sn-1ne2  42703  sqmid3api  42715  re1m1e0m0  42829  sn-0tie0  42896  fltnltalem  43095  unitadd  44622  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  3exp4mod41  48079  bgoldbtbndlem1  48281