Theorem addassi 9927

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

Syntax hints:   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  mul02lem2  10092  addid1  10095  2p2e4  11021  3p2e5  11037  3p3e6  11038  4p2e6  11039  4p3e7  11040  4p4e8  11041  5p2e7  11042  5p3e8  11043  5p4e9  11044  5p5e10OLD  11045  6p2e8  11046  6p3e9  11047  6p4e10OLD  11048  7p2e9  11049  7p3e10OLD  11050  8p2e10OLD  11051  numsuc  11387  nummac  11434  numaddc  11437  6p5lem  11471  5p5e10  11472  6p4e10  11474  7p3e10  11479  8p2e10  11486  binom2i  12836  faclbnd4lem1  12942  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  gcdaddmlem  15083  mod2xnegi  15613  decexp2  15617  decsplit  15625  decsplitOLD  15629  lgsdir2lem2  24851  2lgsoddprmlem3d  24938  ax5seglem7  25615  normlem3  27353  stadd3i  28491  quad3  30818  unitadd  37520  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  3exp4mod41  40071  bgoldbtbndlem1  40221