Theorem addass 11271

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187

This theorem was proved from axioms:  ax-addass 11249

This theorem is referenced by:  addassi  11300  addassd  11312  00id  11465  addlid  11473  add12  11507  add32  11508  add32r  11509  add4  11510  nnaddcl  12316  uzaddcl  12969  xaddass  13311  fztp  13640  seradd  14095  expadd  14155  bernneq  14278  faclbnd6  14348  hashgadd  14426  swrds2  14989  clim2ser  15703  clim2ser2  15704  summolem3  15762  isumsplit  15888  fsumcube  16108  odd2np1lem  16388  prmlem0  17153  cnaddablx  19910  cnaddabl  19911  zaddablx  19914  cncrng  21424  cncrngOLD  21425  cnlmod  25192  pjthlem1  25490  ptolemy  26556  bcp1ctr  27341  cnaddabloOLD  30613  pjhthlem1  31423  dnibndlem5  36448  mblfinlem2  37618  facp2  42100  fac2xp3  42196  2xp3dxp2ge1d  42198  factwoffsmonot  42199  mogoldbblem  47594  nnsgrp  47900  nn0mnd  47902  2zrngasgrp  47969