Theorem addass 11194

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   + caddc 11110

This theorem was proved from axioms:  ax-addass 11172

This theorem is referenced by:  addassi  11221  addassd  11233  00id  11386  addlid  11394  add12  11428  add32  11429  add32r  11430  add4  11431  nnaddcl  12232  uzaddcl  12885  xaddass  13225  fztp  13554  seradd  14007  expadd  14067  bernneq  14189  faclbnd6  14256  hashgadd  14334  swrds2  14888  clim2ser  15598  clim2ser2  15599  summolem3  15657  isumsplit  15783  fsumcube  16001  odd2np1lem  16280  prmlem0  17036  cnaddablx  19731  cnaddabl  19732  zaddablx  19735  cncrng  20959  cnlmod  24648  pjthlem1  24946  ptolemy  25998  bcp1ctr  26772  cnaddabloOLD  29822  pjhthlem1  30632  dnibndlem5  35347  mblfinlem2  36515  facp2  40948  fac2xp3  41009  2xp3dxp2ge1d  41011  factwoffsmonot  41012  mogoldbblem  46375  nnsgrp  46574  nn0mnd  46576  2zrngasgrp  46792