Theorem addass 11183

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  (class class class)co 7408  ℂcc 11094   + caddc 11099

This theorem was proved from axioms:  ax-addass 11161

This theorem is referenced by:  addassi  11215  addassd  11227  00id  11381  addlid  11389  add12  11424  add32  11425  add32r  11426  add4  11427  nnaddcl  12252  uzaddcl  12924  xaddass  13271  fztp  13604  seradd  14076  expadd  14136  bernneq  14261  faclbnd6  14331  hashgadd  14409  swrds2  14973  clim2ser  15702  clim2ser2  15703  summolem3  15761  isumsplit  15890  fsumcube  16110  odd2np1lem  16394  prmlem0  17161  cnaddablx  19934  cnaddabl  19935  zaddablx  19938  cncrng  21508  cnlmod  25264  pjthlem1  25561  ptolemy  26623  bcp1ctr  27405  cnaddabloOLD  30870  pjhthlem1  31680  dnibndlem5  36956  mblfinlem2  38192  facp2  42795  mogoldbblem  48369  nnsgrp  48826  nn0mnd  48828  2zrngasgrp  48895