Theorem addass 11104

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11015   + caddc 11020

This theorem was proved from axioms:  ax-addass 11082

This theorem is referenced by:  addassi  11133  addassd  11145  00id  11299  addlid  11307  add12  11342  add32  11343  add32r  11344  add4  11345  nnaddcl  12159  uzaddcl  12808  xaddass  13155  fztp  13487  seradd  13958  expadd  14018  bernneq  14143  faclbnd6  14213  hashgadd  14291  swrds2  14854  clim2ser  15569  clim2ser2  15570  summolem3  15628  isumsplit  15754  fsumcube  15974  odd2np1lem  16258  prmlem0  17024  cnaddablx  19788  cnaddabl  19789  zaddablx  19792  cncrng  21334  cncrngOLD  21335  cnlmod  25087  pjthlem1  25384  ptolemy  26452  bcp1ctr  27237  cnaddabloOLD  30582  pjhthlem1  31392  dnibndlem5  36598  mblfinlem2  37771  facp2  42309  mogoldbblem  47882  nnsgrp  48339  nn0mnd  48341  2zrngasgrp  48408