Theorem addassi 11264

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

Syntax hints:   = wceq 1534   ∈ wcel 2099  (class class class)co 7415  ℂcc 11146   + caddc 11151

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

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

This theorem is referenced by:  mul02lem2  11431  addrid  11434  2p2e4  12392  1p2e3  12400  3p2e5  12408  3p3e6  12409  4p2e6  12410  4p3e7  12411  4p4e8  12412  5p2e7  12413  5p3e8  12414  5p4e9  12415  6p2e8  12416  6p3e9  12417  7p2e9  12418  numsuc  12736  nummac  12767  numaddc  12770  6p5lem  12792  5p5e10  12793  6p4e10  12794  7p3e10  12797  8p2e10  12802  binom2i  14223  faclbnd4lem1  14304  3dvdsdec  16328  3dvds2dec  16329  gcdaddmlem  16518  mod2xnegi  17067  decexp2  17071  decsplit  17079  lgsdir2lem2  27351  2lgsoddprmlem3d  27438  ax5seglem7  28865  normlem3  31041  stadd3i  32177  dfdec100  32733  dp3mul10  32761  dpmul  32776  dpmul4  32777  quad3  35510  addassnni  41695  sn-1ne2  42003  sqmid3api  42021  re1m1e0m0  42107  sn-0tie0  42149  fltnltalem  42351  unitadd  43898  sqwvfoura  45884  sqwvfourb  45885  fouriersw  45887  3exp4mod41  47223  bgoldbtbndlem1  47412