Theorem addassi 10387

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

Syntax hints:   = wceq 1601   ∈ wcel 2107  (class class class)co 6922  ℂcc 10270   + caddc 10275

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-3an 1073

This theorem is referenced by:  mul02lem2  10553  addid1  10556  2p2e4  11517  1p2e3  11525  3p2e5  11533  3p3e6  11534  4p2e6  11535  4p3e7  11536  4p4e8  11537  5p2e7  11538  5p3e8  11539  5p4e9  11540  6p2e8  11541  6p3e9  11542  7p2e9  11543  numsuc  11859  nummac  11891  numaddc  11894  6p5lem  11917  5p5e10  11918  6p4e10  11919  7p3e10  11922  8p2e10  11927  binom2i  13293  faclbnd4lem1  13398  3dvdsdec  15460  3dvds2dec  15461  gcdaddmlem  15651  mod2xnegi  16179  decexp2  16183  decsplit  16191  lgsdir2lem2  25503  2lgsoddprmlem3d  25590  ax5seglem7  26284  normlem3  28541  stadd3i  29679  dfdec100  30140  dp3mul10  30168  dpmul  30183  dpmul4  30184  quad3  32161  sqmid3api  38149  unitadd  39454  sqwvfoura  41372  sqwvfourb  41373  fouriersw  41375  3exp4mod41  42554  bgoldbtbndlem1  42718