Theorem addass 11182

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   + caddc 11098

This theorem was proved from axioms:  ax-addass 11160

This theorem is referenced by:  addassi  11214  addassd  11226  00id  11380  addlid  11388  add12  11423  add32  11424  add32r  11425  add4  11426  nnaddcl  12251  uzaddcl  12923  xaddass  13270  fztp  13604  seradd  14076  expadd  14136  bernneq  14261  faclbnd6  14331  hashgadd  14409  swrds2  14973  clim2ser  15702  clim2ser2  15703  summolem3  15761  isumsplit  15890  fsumcube  16109  odd2np1lem  16393  prmlem0  17160  cnaddablx  19933  cnaddabl  19934  zaddablx  19937  cncrng  21543  cnlmod  25299  pjthlem1  25596  ptolemy  26661  bcp1ctr  27443  cnaddabloOLD  30933  pjhthlem1  31743  dnibndlem5  37071  mblfinlem2  38309  facp2  42910  mogoldbblem  48485  nnsgrp  48942  nn0mnd  48944  2zrngasgrp  49011