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

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

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 10590 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   + caddc 10528
This theorem was proved from axioms:  ax-addass 10590
This theorem is referenced by:  addassi  10639  addassd  10651  00id  10803  addid2  10811  add12  10845  add32  10846  add32r  10847  add4  10848  nnaddcl  11648  uzaddcl  12292  xaddass  12630  fztp  12951  seradd  13400  expadd  13459  bernneq  13578  faclbnd6  13647  hashgadd  13726  swrds2  14290  clim2ser  14999  clim2ser2  15000  summolem3  15059  isumsplit  15183  fsumcube  15402  odd2np1lem  15677  prmlem0  16427  cnaddablx  18917  cnaddabl  18918  zaddablx  18921  cncrng  20494  cnlmod  23671  pjthlem1  23967  ptolemy  25009  bcp1ctr  25782  cnaddabloOLD  28285  pjhthlem1  29095  dnibndlem5  33718  mblfinlem2  34811  mogoldbblem  43762  nnsgrp  43961  nn0mnd  43963  2zrngasgrp  44139
  Copyright terms: Public domain W3C validator