Theorem addassi 8053

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

Syntax hints:   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   + caddc 7901

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 8000

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

This theorem is referenced by:  2p2e4  9136  3p2e5  9151  3p3e6  9152  4p2e6  9153  4p3e7  9154  4p4e8  9155  5p2e7  9156  5p3e8  9157  5p4e9  9158  6p2e8  9159  6p3e9  9160  7p2e9  9161  numsuc  9489  nummac  9520  numaddc  9523  6p5lem  9545  5p5e10  9546  6p4e10  9547  7p3e10  9550  8p2e10  9555  binom2i  10759  resqrexlemover  11194  3dvdsdec  12049  3dvds2dec  12050  decsplit  12625  lgsdir2lem2  15356  2lgsoddprmlem3d  15437