Theorem addassi 11156

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7370  ℂcc 11038   + caddc 11043

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

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

This theorem is referenced by:  mul02lem2  11324  addrid  11327  2p2e4  12289  1p2e3  12297  3p2e5  12305  3p3e6  12306  4p2e6  12307  4p3e7  12308  4p4e8  12309  5p2e7  12310  5p3e8  12311  5p4e9  12312  6p2e8  12313  6p3e9  12314  7p2e9  12315  numsuc  12635  nummac  12666  numaddc  12669  6p5lem  12691  5p5e10  12692  6p4e10  12693  7p3e10  12696  8p2e10  12701  binom2i  14149  faclbnd4lem1  14230  3dvdsdec  16273  3dvds2dec  16274  gcdaddmlem  16465  mod2xnegi  17013  decsplit  17024  lgsdir2lem2  27310  2lgsoddprmlem3d  27397  ax5seglem7  29026  normlem3  31206  stadd3i  32342  dfdec100  32928  dp3mul10  32996  dpmul  33011  dpmul4  33012  cos9thpiminplylem4  33969  quad3  35892  addassnni  42383  1p3e4  42658  sn-1ne2  42664  sqmid3api  42682  re1m1e0m0  42796  sn-0tie0  42850  fltnltalem  43049  unitadd  44580  sqwvfoura  46615  sqwvfourb  46616  fouriersw  46618  3exp4mod41  48005  bgoldbtbndlem1  48194