Theorem addassi 11268

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7416  ℂcc 11147   + caddc 11152

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

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

This theorem is used by:  mul02lem2  11436  addrid  11439  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  12775  nummac  12811  numaddc  12814  6p5lem  12836  5p5e10  12837  6p4e10  12838  7p3e10  12841  8p2e10  12846  binom2i  14301  faclbnd4lem1  14382  3dvdsdec  16447  3dvds2dec  16448  gcdaddmlem  16639  mod2xnegi  17188  decsplit  17199  lgsdir2lem2  27594  2lgsoddprmlem3d  27681  ax5seglem7  29424  normlem3  31625  stadd3i  32761  dfdec100  33332  dp3mul10  33375  dpmul  33390  dpmul4  33391  cos9thpiminplylem4  34328  quad3  36332  addassnni  42915  4p4e8ALT  43190  1p3e4  43191  1p4e5  43192  1p5e6  43193  1p6e7  43194  1p7e8  43195  1p8e9  43196  2p3e5  43197  2p4e6  43198  2p5e7  43199  2p6e8  43200  2p7e9  43201  3p4e7  43202  3p5e8  43203  3p6e9  43204  4p5e9  43205  sn-1ne2  43211  sqmid3api  43223  re1m1e0m0  43337  sn-0tie0  43404  fltnltalem  43573  unitadd  45100  sqwvfoura  47121  sqwvfourb  47122  fouriersw  47124  goldpolyfactor  47810  3exp4mod41  48584  bgoldbtbndlem1  48786