Theorem addass 7165

Description: Alias for ax-addass 7140, for naming consistency with addassi 7189. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
addass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addass

Step	Hyp	Ref	Expression
1		ax-addass 7140	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Syntax hints:   → wi 4   ∧ w3a 920   = wceq 1285   ∈ wcel 1434  (class class class)co 5543  ℂcc 7041   + caddc 7046

This theorem was proved from axioms:  ax-addass 7140

This theorem is referenced by:  addassi  7189  addassd  7203  add12  7333  add32  7334  add32r  7335  add4  7336  nnaddcl  8126  uzaddcl  8755  fztp  9171  iseradd  9559  expadd  9615  bernneq  9690  faclbnd6  9768  resqrexlemover  10034  clim2iser  10313  clim2iser2  10314  odd2np1lem  10416