Theorem addass 11199

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   + caddc 11115

This theorem was proved from axioms:  ax-addass 11177

This theorem is referenced by:  addassi  11228  addassd  11240  00id  11393  addlid  11401  add12  11435  add32  11436  add32r  11437  add4  11438  nnaddcl  12239  uzaddcl  12892  xaddass  13232  fztp  13561  seradd  14014  expadd  14074  bernneq  14196  faclbnd6  14263  hashgadd  14341  swrds2  14895  clim2ser  15605  clim2ser2  15606  summolem3  15664  isumsplit  15790  fsumcube  16008  odd2np1lem  16287  prmlem0  17043  cnaddablx  19777  cnaddabl  19778  zaddablx  19781  cncrng  21166  cnlmod  24887  pjthlem1  25185  ptolemy  26242  bcp1ctr  27018  cnaddabloOLD  30101  pjhthlem1  30911  gg-cncrng  35486  dnibndlem5  35661  mblfinlem2  36829  facp2  41265  fac2xp3  41326  2xp3dxp2ge1d  41328  factwoffsmonot  41329  mogoldbblem  46686  nnsgrp  46853  nn0mnd  46855  2zrngasgrp  46926