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

Theorem addassd 9918
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 9879 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4syl3anc 1317 1 (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  (class class class)co 6527  cc 9790   + caddc 9795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9857
This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032
This theorem is referenced by:  addid1  10067  cnegex  10068  addid2  10070  addcan  10071  addcan2  10072  addcom  10073  addcomd  10089  muladd11r  10100  negeu  10122  addsubass  10142  nppcan3  10156  muladd  10313  add1p1  11130  div4p1lem1div2  11134  zpnn0elfzo1  12363  flhalf  12448  fldiv  12476  binom3  12802  bernneq  12807  discr1  12817  ccatass  13170  cshweqrep  13364  sqrlem7  13783  sqreulem  13893  isercoll2  14193  caucvgrlem  14197  iseraltlem2  14207  bcxmas  14352  bpoly4  14575  efsep  14625  efi4p  14652  efival  14667  pwp1fsum  14898  flodddiv4  14921  sadadd2lem2  14956  sadadd2lem  14965  sadasslem  14976  pcadd2  15378  prmreclem6  15409  4sqlem11  15443  vdwapun  15462  vdwlem3  15471  vdwlem6  15474  vdwlem8  15476  vdwlem9  15477  prmgaplem8  15546  psgnunilem2  17684  sylow1lem1  17782  efgredlemc  17927  opnreen  22374  ovolunlem1a  22988  nulmbl2  23028  unmbl  23029  volinun  23038  uniioombllem5  23078  itgcnlem  23279  ditgsplit  23348  dvnadd  23415  dvntaylp  23846  ulmshft  23865  ulmcn  23874  tangtx  23978  heron  24282  quad2  24283  dcubic1lem  24287  mcubic  24291  binom4  24294  dquartlem1  24295  dquartlem2  24296  dquart  24297  quart1  24300  quart  24305  lgamcvg2  24498  basellem2  24525  basellem3  24526  basellem8  24531  ppiub  24646  bcp1ctr  24721  bposlem9  24734  2lgslem3c  24840  2lgslem3d  24841  selberg3  24965  pntpbnd2  24993  pntibndlem2  24997  pntlemg  25004  pntlemk  25012  pntlemo  25013  axeuclidlem  25560  axcontlem2  25563  axcontlem4  25565  axcontlem7  25568  wwlkextwrd  26022  wwlkextproplem3  26037  wwlkext2clwwlk  26097  numclwlk1lem2fo  26388  numclwlk2lem2f  26396  numclwlk2lem2f1o  26398  smcnlem  26737  stadd3i  28297  golem1  28320  archirngz  28880  subfacval2  30229  subfaclim  30230  subfacval3  30231  faclimlem1  30688  faclim2  30693  fwddifnp1  31248  dnizphlfeqhlf  31442  dnibndlem10  31453  dnibndlem13  31456  poimirlem16  32391  itg2addnclem3  32429  itg2addnc  32430  areacirclem1  32466  jm2.19lem3  36372  jm2.25  36380  int-addassocd  37295  binomcxplemnotnn0  37373  sub2times  38222  fperiodmullem  38254  dvnmul  38630  wallispilem4  38758  wallispi2lem2  38762  stirlinglem6  38769  dirkerper  38786  dirkertrigeqlem1  38788  dirkertrigeqlem2  38789  dirkertrigeqlem3  38790  dirkercncflem1  38793  fourierdlem26  38823  fourierdlem35  38832  fourierdlem42  38839  fourierdlem51  38847  fourierdlem64  38860  fourierdlem111  38907  hoidmv1lelem2  39279  hoidmvlelem2  39283  smflimlem4  39457  deccarry  39739  sqrtpwpw2p  39786  fmtnorec2lem  39790  fmtnorec3  39796  fmtnorec4  39797  mod42tp1mod8  39855  wwlksnextwrd  41098  wwlksnextproplem3  41112  wwlksext2clwwlk  41226  av-numclwlk1lem2fo  41520  av-numclwlk2lem2f  41528  av-numclwlk2lem2f1o  41530  sinhpcosh  42236
  Copyright terms: Public domain W3C validator