Theorem addass 11242

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   + caddc 11158

This theorem was proved from axioms:  ax-addass 11220

This theorem is referenced by:  addassi  11271  addassd  11283  00id  11436  addlid  11444  add12  11479  add32  11480  add32r  11481  add4  11482  nnaddcl  12289  uzaddcl  12946  xaddass  13291  fztp  13620  seradd  14085  expadd  14145  bernneq  14268  faclbnd6  14338  hashgadd  14416  swrds2  14979  clim2ser  15691  clim2ser2  15692  summolem3  15750  isumsplit  15876  fsumcube  16096  odd2np1lem  16377  prmlem0  17143  cnaddablx  19886  cnaddabl  19887  zaddablx  19890  cncrng  21401  cncrngOLD  21402  cnlmod  25173  pjthlem1  25471  ptolemy  26538  bcp1ctr  27323  cnaddabloOLD  30600  pjhthlem1  31410  dnibndlem5  36483  mblfinlem2  37665  facp2  42144  fac2xp3  42240  2xp3dxp2ge1d  42242  factwoffsmonot  42243  mogoldbblem  47707  nnsgrp  48093  nn0mnd  48095  2zrngasgrp  48162