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

Theorem addassd 10254
Description: Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
addassd.3 (𝜑𝐶 ∈ ℂ)
Assertion
Ref Expression
addassd (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addassd
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addassd.3 . 2 (𝜑𝐶 ∈ ℂ)
4 addass 10215 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4syl3anc 1477 1 (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  (class class class)co 6813  cc 10126   + caddc 10131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 10193
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074
This theorem is referenced by:  addid1  10408  cnegex  10409  addid2  10411  addcan  10412  addcan2  10413  addcom  10414  addcomd  10430  muladd11r  10441  negeu  10463  addsubass  10483  nppcan3  10497  muladd  10654  add1p1  11475  div4p1lem1div2  11479  zpnn0elfzo1  12736  flhalf  12825  fldiv  12853  binom3  13179  bernneq  13184  discr1  13194  ccatass  13560  cshweqrep  13767  sqrlem7  14188  sqreulem  14298  isercoll2  14598  caucvgrlem  14602  iseraltlem2  14612  bcxmas  14766  bpoly4  14989  efsep  15039  efi4p  15066  efival  15081  pwp1fsum  15316  flodddiv4  15339  sadadd2lem2  15374  sadadd2lem  15383  sadasslem  15394  pcadd2  15796  prmreclem6  15827  4sqlem11  15861  vdwapun  15880  vdwlem3  15889  vdwlem6  15892  vdwlem8  15894  vdwlem9  15895  prmgaplem8  15964  psgnunilem2  18115  sylow1lem1  18213  efgredlemc  18358  opnreen  22835  ovolunlem1a  23464  nulmbl2  23504  unmbl  23505  volinun  23514  uniioombllem5  23555  itgcnlem  23755  ditgsplit  23824  dvnadd  23891  dvntaylp  24324  ulmshft  24343  ulmcn  24352  tangtx  24456  heron  24764  quad2  24765  dcubic1lem  24769  mcubic  24773  binom4  24776  dquartlem1  24777  dquartlem2  24778  dquart  24779  quart1  24782  quart  24787  lgamcvg2  24980  basellem2  25007  basellem3  25008  basellem8  25013  ppiub  25128  bcp1ctr  25203  bposlem9  25216  2lgslem3c  25322  2lgslem3d  25323  selberg3  25447  pntpbnd2  25475  pntibndlem2  25479  pntlemg  25486  pntlemk  25494  pntlemo  25495  axeuclidlem  26041  axcontlem2  26044  axcontlem4  26046  axcontlem7  26049  finsumvtxdg2ssteplem4  26654  wwlksnextwrd  27015  wwlksnextproplem3  27029  wwlksext2clwwlk  27187  wwlksext2clwwlkOLD  27188  numclwlk2lem2f  27538  numclwlk2lem2f1o  27540  numclwlk2lem2fOLD  27545  numclwlk2lem2f1oOLD  27547  smcnlem  27861  stadd3i  29416  golem1  29439  archirngz  30052  subfacval2  31476  subfaclim  31477  subfacval3  31478  faclimlem1  31936  faclim2  31941  fwddifnp1  32578  dnizphlfeqhlf  32772  dnibndlem10  32783  dnibndlem13  32786  poimirlem16  33738  itg2addnclem3  33776  itg2addnc  33777  areacirclem1  33813  jm2.19lem3  38060  jm2.25  38068  int-addassocd  38979  binomcxplemnotnn0  39057  sub2times  39984  fperiodmullem  40016  dvnmul  40661  wallispilem4  40788  wallispi2lem2  40792  stirlinglem6  40799  dirkerper  40816  dirkertrigeqlem1  40818  dirkertrigeqlem2  40819  dirkertrigeqlem3  40820  dirkercncflem1  40823  fourierdlem26  40853  fourierdlem35  40862  fourierdlem42  40869  fourierdlem51  40877  fourierdlem64  40890  fourierdlem111  40937  hoidmv1lelem2  41312  hoidmvlelem2  41316  smflimlem4  41488  deccarry  41831  sqrtpwpw2p  41960  fmtnorec2lem  41964  fmtnorec3  41970  fmtnorec4  41971  mod42tp1mod8  42029  sinhpcosh  42994
  Copyright terms: Public domain W3C validator