Theorem addassi 11239

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  (class class class)co 7420  ℂcc 11118   + caddc 11123

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

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

This theorem is used by:  mul02lem2  11407  addrid  11410  2p2e4  12395  1p2e3  12403  3p2e5  12411  3p3e6  12412  4p2e6  12413  4p3e7  12414  4p4e8  12415  5p2e7  12416  5p3e8  12417  5p4e9  12418  6p2e8  12419  6p3e9  12420  7p2e9  12421  numsuc  12746  nummac  12782  numaddc  12785  6p5lem  12807  5p5e10  12808  6p4e10  12809  7p3e10  12812  8p2e10  12817  binom2i  14271  faclbnd4lem1  14352  3dvdsdec  16417  3dvds2dec  16418  gcdaddmlem  16609  mod2xnegi  17158  decsplit  17169  lgsdir2lem2  27546  2lgsoddprmlem3d  27633  ax5seglem7  29345  normlem3  31540  stadd3i  32676  dfdec100  33249  dp3mul10  33292  dpmul  33307  dpmul4  33308  cos9thpiminplylem4  34244  quad3  36204  addassnni  42814  4p4e8ALT  43089  1p3e4  43090  1p4e5  43091  1p5e6  43092  1p6e7  43093  1p7e8  43094  1p8e9  43095  2p3e5  43096  2p4e6  43097  2p5e7  43098  2p6e8  43099  2p7e9  43100  3p4e7  43101  3p5e8  43102  3p6e9  43103  4p5e9  43104  sn-1ne2  43110  sqmid3api  43122  re1m1e0m0  43236  sn-0tie0  43303  fltnltalem  43472  unitadd  44999  sqwvfoura  47020  sqwvfourb  47021  fouriersw  47023  3exp4mod41  48446  bgoldbtbndlem1  48648