Theorem addass 11326

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

Assertion

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

Proof of Theorem addass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237   + caddc 11242

This proof depends on axioms:  ax-addass 11304

This theorem is used by:  addassi  11358  addassd  11370  00id  11524  addlid  11532  add12  11567  add32  11568  add32r  11569  add4  11570  nnaddcl  12398  uzaddcl  13071  xaddass  13419  fztp  13754  seradd  14227  expadd  14287  bernneq  14414  faclbnd6  14484  hashgadd  14562  swrds2  15134  clim2ser  15866  clim2ser2  15867  summolem3  15924  isumsplit  16053  fsumcube  16270  odd2np1lem  16554  prmlem0  17327  cnaddablx  20133  cnaddabl  20134  zaddablx  20137  cncrng  21751  cnlmod  25516  pjthlem1  25813  ptolemy  26882  bcp1ctr  27663  cnaddabloOLD  31240  pjhthlem1  32050  dnibndlem5  37563  mblfinlem2  38844  facp2  43459  mogoldbblem  49091  nnsgrp  49547  nn0mnd  49549  2zrngasgrp  49616