Theorem addass 10702

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114  (class class class)co 7170  ℂcc 10613   + caddc 10618

This theorem was proved from axioms:  ax-addass 10680

This theorem is referenced by:  addassi  10729  addassd  10741  00id  10893  addid2  10901  add12  10935  add32  10936  add32r  10937  add4  10938  nnaddcl  11739  uzaddcl  12386  xaddass  12725  fztp  13054  seradd  13504  expadd  13563  bernneq  13682  faclbnd6  13751  hashgadd  13830  swrds2  14391  clim2ser  15104  clim2ser2  15105  summolem3  15164  isumsplit  15288  fsumcube  15506  odd2np1lem  15785  prmlem0  16542  cnaddablx  19107  cnaddabl  19108  zaddablx  19111  cncrng  20238  cnlmod  23892  pjthlem1  24189  ptolemy  25241  bcp1ctr  26015  cnaddabloOLD  28516  pjhthlem1  29326  dnibndlem5  34300  mblfinlem2  35438  facp2  39705  fac2xp3  39751  2xp3dxp2ge1d  39753  factwoffsmonot  39754  mogoldbblem  44706  nnsgrp  44905  nn0mnd  44907  2zrngasgrp  45032