Theorem addassi 11247

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   + caddc 11131

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11193

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mul02lem2  11415  addrid  11418  2p2e4  12403  1p2e3  12411  3p2e5  12419  3p3e6  12420  4p2e6  12421  4p3e7  12422  4p4e8  12423  5p2e7  12424  5p3e8  12425  5p4e9  12426  6p2e8  12427  6p3e9  12428  7p2e9  12429  numsuc  12754  nummac  12790  numaddc  12793  6p5lem  12815  5p5e10  12816  6p4e10  12817  7p3e10  12820  8p2e10  12825  binom2i  14280  faclbnd4lem1  14361  3dvdsdec  16428  3dvds2dec  16429  gcdaddmlem  16620  mod2xnegi  17169  decsplit  17180  lgsdir2lem2  27570  2lgsoddprmlem3d  27657  ax5seglem7  29400  normlem3  31601  stadd3i  32737  dfdec100  33308  dp3mul10  33351  dpmul  33366  dpmul4  33367  cos9thpiminplylem4  34303  quad3  36257  addassnni  42858  4p4e8ALT  43133  1p3e4  43134  1p4e5  43135  1p5e6  43136  1p6e7  43137  1p7e8  43138  1p8e9  43139  2p3e5  43140  2p4e6  43141  2p5e7  43142  2p6e8  43143  2p7e9  43144  3p4e7  43145  3p5e8  43146  3p6e9  43147  4p5e9  43148  sn-1ne2  43154  sqmid3api  43166  re1m1e0m0  43280  sn-0tie0  43347  fltnltalem  43516  unitadd  45043  sqwvfoura  47064  sqwvfourb  47065  fouriersw  47067  goldpolyfactor  47753  3exp4mod41  48527  bgoldbtbndlem1  48729