Theorem addassi 11278

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  (class class class)co 7438  ℂcc 11160   + caddc 11165

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  mul02lem2  11445  addrid  11448  2p2e4  12408  1p2e3  12416  3p2e5  12424  3p3e6  12425  4p2e6  12426  4p3e7  12427  4p4e8  12428  5p2e7  12429  5p3e8  12430  5p4e9  12431  6p2e8  12432  6p3e9  12433  7p2e9  12434  numsuc  12754  nummac  12785  numaddc  12788  6p5lem  12810  5p5e10  12811  6p4e10  12812  7p3e10  12815  8p2e10  12820  binom2i  14257  faclbnd4lem1  14338  3dvdsdec  16375  3dvds2dec  16376  gcdaddmlem  16567  mod2xnegi  17114  decexp2  17118  decsplit  17126  lgsdir2lem2  27396  2lgsoddprmlem3d  27483  ax5seglem7  28976  normlem3  31157  stadd3i  32293  dfdec100  32851  dp3mul10  32897  dpmul  32912  dpmul4  32913  quad3  35668  addassnni  41980  sn-1ne2  42293  sqmid3api  42311  re1m1e0m0  42420  sn-0tie0  42462  fltnltalem  42665  unitadd  44201  sqwvfoura  46212  sqwvfourb  46213  fouriersw  46215  3exp4mod41  47569  bgoldbtbndlem1  47758