Theorem addassi 8080

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

Syntax hints:   = wceq 1373   ∈ wcel 2176  (class class class)co 5944  ℂcc 7923   + caddc 7928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 8027

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  2p2e4  9163  3p2e5  9178  3p3e6  9179  4p2e6  9180  4p3e7  9181  4p4e8  9182  5p2e7  9183  5p3e8  9184  5p4e9  9185  6p2e8  9186  6p3e9  9187  7p2e9  9188  numsuc  9517  nummac  9548  numaddc  9551  6p5lem  9573  5p5e10  9574  6p4e10  9575  7p3e10  9578  8p2e10  9583  binom2i  10793  resqrexlemover  11321  3dvdsdec  12176  3dvds2dec  12177  decsplit  12752  lgsdir2lem2  15506  2lgsoddprmlem3d  15587