Theorem addassi 11319

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11198   + caddc 11203

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

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

This theorem is used by:  mul02lem2  11487  addrid  11490  2p2e4  12477  1p2e3  12485  3p2e5  12493  3p3e6  12494  4p2e6  12495  4p3e7  12496  4p4e8  12497  5p2e7  12498  5p3e8  12499  5p4e9  12500  6p2e8  12501  6p3e9  12502  7p2e9  12503  numsuc  12828  nummac  12864  numaddc  12867  6p5lem  12889  5p5e10  12890  6p4e10  12891  7p3e10  12894  8p2e10  12899  binom2i  14356  faclbnd4lem1  14437  3dvdsdec  16502  3dvds2dec  16503  gcdaddmlem  16696  mod2xnegi  17249  decsplit  17260  lgsdir2lem2  27653  2lgsoddprmlem3d  27740  ax5seglem7  29513  normlem3  31714  stadd3i  32850  dfdec100  33421  dp3mul10  33464  dpmul  33479  dpmul4  33480  cos9thpiminplylem4  34417  quad3  36435  addassnni  43035  4p4e8ALT  43310  1p3e4  43311  1p4e5  43312  1p5e6  43313  1p6e7  43314  1p7e8  43315  1p8e9  43316  2p3e5  43317  2p4e6  43318  2p5e7  43319  2p6e8  43320  2p7e9  43321  3p4e7  43322  3p5e8  43323  3p6e9  43324  4p5e9  43325  sn-1ne2  43331  sqmid3api  43341  re1m1e0m0  43449  sn-0tie0  43516  fltnltalem  43674  unitadd  45195  sqwvfoura  47238  sqwvfourb  47239  fouriersw  47241  goldpolyfactor  47927  3exp4mod41  48701  bgoldbtbndlem1  48903