Theorem addassi 10916

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   + caddc 10805

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  mul02lem2  11082  addid1  11085  2p2e4  12038  1p2e3  12046  3p2e5  12054  3p3e6  12055  4p2e6  12056  4p3e7  12057  4p4e8  12058  5p2e7  12059  5p3e8  12060  5p4e9  12061  6p2e8  12062  6p3e9  12063  7p2e9  12064  numsuc  12380  nummac  12411  numaddc  12414  6p5lem  12436  5p5e10  12437  6p4e10  12438  7p3e10  12441  8p2e10  12446  binom2i  13856  faclbnd4lem1  13935  3dvdsdec  15969  3dvds2dec  15970  gcdaddmlem  16159  mod2xnegi  16700  decexp2  16704  decsplit  16712  lgsdir2lem2  26379  2lgsoddprmlem3d  26466  ax5seglem7  27206  normlem3  29375  stadd3i  30511  dfdec100  31046  dp3mul10  31074  dpmul  31089  dpmul4  31090  quad3  33528  addassnni  39921  sn-1ne2  40216  sqmid3api  40232  re1m1e0m0  40301  sn-0tie0  40342  fltnltalem  40415  unitadd  41695  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  3exp4mod41  44956  bgoldbtbndlem1  45145