MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addass Structured version   Visualization version   GIF version

Theorem addass 10613
Description: Alias for ax-addass 10591, for naming consistency with addassi 10640. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addass ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 10591 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081   = wceq 1530  wcel 2107  (class class class)co 7148  cc 10524   + caddc 10529
This theorem was proved from axioms:  ax-addass 10591
This theorem is referenced by:  addassi  10640  addassd  10652  00id  10804  addid2  10812  add12  10846  add32  10847  add32r  10848  add4  10849  nnaddcl  11649  uzaddcl  12293  xaddass  12632  fztp  12953  seradd  13402  expadd  13461  bernneq  13580  faclbnd6  13649  hashgadd  13728  swrds2  14292  clim2ser  15001  clim2ser2  15002  summolem3  15061  isumsplit  15185  fsumcube  15404  odd2np1lem  15679  prmlem0  16429  cnaddablx  18908  cnaddabl  18909  zaddablx  18912  cncrng  20482  cnlmod  23659  pjthlem1  23955  ptolemy  24997  bcp1ctr  25769  cnaddabloOLD  28272  pjhthlem1  29082  dnibndlem5  33705  mblfinlem2  34797  mogoldbblem  43717  nnsgrp  43916  nn0mnd  43918  2zrngasgrp  44043
  Copyright terms: Public domain W3C validator