Theorem addass 10942

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853   + caddc 10858

This theorem was proved from axioms:  ax-addass 10920

This theorem is referenced by:  addassi  10969  addassd  10981  00id  11133  addid2  11141  add12  11175  add32  11176  add32r  11177  add4  11178  nnaddcl  11979  uzaddcl  12626  xaddass  12965  fztp  13294  seradd  13746  expadd  13806  bernneq  13925  faclbnd6  13994  hashgadd  14073  swrds2  14634  clim2ser  15347  clim2ser2  15348  summolem3  15407  isumsplit  15533  fsumcube  15751  odd2np1lem  16030  prmlem0  16788  cnaddablx  19450  cnaddabl  19451  zaddablx  19454  cncrng  20600  cnlmod  24284  pjthlem1  24582  ptolemy  25634  bcp1ctr  26408  cnaddabloOLD  28922  pjhthlem1  29732  dnibndlem5  34641  mblfinlem2  35794  facp2  40079  fac2xp3  40140  2xp3dxp2ge1d  40142  factwoffsmonot  40143  mogoldbblem  45124  nnsgrp  45323  nn0mnd  45325  2zrngasgrp  45450