Theorem addassi 10653

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   + caddc 10542

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  mul02lem2  10819  addid1  10822  2p2e4  11775  1p2e3  11783  3p2e5  11791  3p3e6  11792  4p2e6  11793  4p3e7  11794  4p4e8  11795  5p2e7  11796  5p3e8  11797  5p4e9  11798  6p2e8  11799  6p3e9  11800  7p2e9  11801  numsuc  12115  nummac  12146  numaddc  12149  6p5lem  12171  5p5e10  12172  6p4e10  12173  7p3e10  12176  8p2e10  12181  binom2i  13577  faclbnd4lem1  13656  3dvdsdec  15683  3dvds2dec  15684  gcdaddmlem  15874  mod2xnegi  16409  decexp2  16413  decsplit  16421  lgsdir2lem2  25904  2lgsoddprmlem3d  25991  ax5seglem7  26723  normlem3  28891  stadd3i  30027  dfdec100  30548  dp3mul10  30576  dpmul  30591  dpmul4  30592  quad3  32915  sn-1ne2  39165  sqmid3api  39176  re1m1e0m0  39234  fltnltalem  39281  unitadd  40555  sqwvfoura  42520  sqwvfourb  42521  fouriersw  42523  3exp4mod41  43788  bgoldbtbndlem1  43977