Theorem addass 11239

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   + caddc 11155

This theorem was proved from axioms:  ax-addass 11217

This theorem is referenced by:  addassi  11268  addassd  11280  00id  11433  addlid  11441  add12  11476  add32  11477  add32r  11478  add4  11479  nnaddcl  12286  uzaddcl  12943  xaddass  13287  fztp  13616  seradd  14081  expadd  14141  bernneq  14264  faclbnd6  14334  hashgadd  14412  swrds2  14975  clim2ser  15687  clim2ser2  15688  summolem3  15746  isumsplit  15872  fsumcube  16092  odd2np1lem  16373  prmlem0  17139  cnaddablx  19900  cnaddabl  19901  zaddablx  19904  cncrng  21418  cncrngOLD  21419  cnlmod  25186  pjthlem1  25484  ptolemy  26552  bcp1ctr  27337  cnaddabloOLD  30609  pjhthlem1  31419  dnibndlem5  36464  mblfinlem2  37644  facp2  42124  fac2xp3  42220  2xp3dxp2ge1d  42222  factwoffsmonot  42223  mogoldbblem  47644  nnsgrp  48020  nn0mnd  48022  2zrngasgrp  48089