Theorem addassi 11296

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

Syntax hints:   = wceq 1537   ∈ wcel 2103  (class class class)co 7445  ℂcc 11178   + caddc 11183

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

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

This theorem is referenced by:  mul02lem2  11463  addrid  11466  2p2e4  12424  1p2e3  12432  3p2e5  12440  3p3e6  12441  4p2e6  12442  4p3e7  12443  4p4e8  12444  5p2e7  12445  5p3e8  12446  5p4e9  12447  6p2e8  12448  6p3e9  12449  7p2e9  12450  numsuc  12768  nummac  12799  numaddc  12802  6p5lem  12824  5p5e10  12825  6p4e10  12826  7p3e10  12829  8p2e10  12834  binom2i  14257  faclbnd4lem1  14338  3dvdsdec  16374  3dvds2dec  16375  gcdaddmlem  16564  mod2xnegi  17113  decexp2  17117  decsplit  17125  lgsdir2lem2  27379  2lgsoddprmlem3d  27466  ax5seglem7  28959  normlem3  31135  stadd3i  32271  dfdec100  32826  dp3mul10  32854  dpmul  32869  dpmul4  32870  quad3  35630  addassnni  41889  sn-1ne2  42202  sqmid3api  42220  re1m1e0m0  42306  sn-0tie0  42348  fltnltalem  42550  unitadd  44097  sqwvfoura  46083  sqwvfourb  46084  fouriersw  46086  3exp4mod41  47422  bgoldbtbndlem1  47611