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

Theorem addassd 10316
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 10276 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4syl3anc 1490 1 (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wcel 2155  (class class class)co 6842  cc 10187   + caddc 10192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 10254
This theorem depends on definitions:  df-bi 198  df-an 385  df-3an 1109
This theorem is referenced by:  addid1  10470  cnegex  10471  addid2  10473  addcan  10474  addcan2  10475  addcom  10476  addcomd  10492  muladd11r  10503  negeu  10525  addsubass  10545  nppcan3  10559  muladd  10716  add1p1  11529  div4p1lem1div2  11533  zpnn0elfzo1  12750  flhalf  12839  fldiv  12867  binom3  13192  bernneq  13197  discr1  13207  ccatass  13559  cshweqrep  13850  sqrlem7  14274  sqreulem  14384  isercoll2  14684  caucvgrlem  14688  iseraltlem2  14698  bcxmas  14851  bpoly4  15072  efsep  15122  efi4p  15149  efival  15164  pwp1fsum  15396  flodddiv4  15418  sadadd2lem2  15453  sadadd2lem  15462  sadasslem  15473  pcadd2  15873  prmreclem6  15904  4sqlem11  15938  vdwapun  15957  vdwlem3  15966  vdwlem6  15969  vdwlem8  15971  vdwlem9  15972  prmgaplem8  16041  psgnunilem2  18179  sylow1lem1  18277  efgredlemc  18423  opnreen  22913  ovolunlem1a  23554  nulmbl2  23594  unmbl  23595  volinun  23604  uniioombllem5  23645  itgcnlem  23847  ditgsplit  23916  dvnadd  23983  dvntaylp  24416  ulmshft  24435  ulmcn  24444  tangtx  24549  heron  24856  quad2  24857  dcubic1lem  24861  mcubic  24865  binom4  24868  dquartlem1  24869  dquartlem2  24870  dquart  24871  quart1  24874  quart  24879  lgamcvg2  25072  basellem2  25099  basellem3  25100  basellem8  25105  ppiub  25220  bcp1ctr  25295  bposlem9  25308  2lgslem3c  25414  2lgslem3d  25415  selberg3  25539  pntpbnd2  25567  pntibndlem2  25571  pntlemg  25578  pntlemk  25586  pntlemo  25587  axeuclidlem  26133  axcontlem2  26136  axcontlem4  26138  axcontlem7  26141  finsumvtxdg2ssteplem4  26735  wwlksnextwrd  27103  wwlksnextwrdOLD  27108  wwlksnextproplem3  27128  wwlksnextproplem3OLD  27129  wwlksext2clwwlk  27307  wwlksext2clwwlkOLD  27308  numclwlk2lem2f  27681  numclwlk2lem2f1o  27683  numclwlk2lem2fOLD  27684  numclwlk2lem2f1oOLD  27686  numclwlk2lem2fOLDOLD  27692  numclwlk2lem2f1oOLDOLD  27694  smcnlem  28008  stadd3i  29563  golem1  29586  archirngz  30190  subfacval2  31617  subfaclim  31618  subfacval3  31619  faclimlem1  32074  faclim2  32079  fwddifnp1  32716  dnizphlfeqhlf  32905  dnibndlem10  32916  dnibndlem13  32919  poimirlem16  33849  itg2addnclem3  33886  itg2addnc  33887  areacirclem1  33923  jm2.19lem3  38235  jm2.25  38243  int-addassocd  39151  binomcxplemnotnn0  39229  sub2times  40126  fperiodmullem  40156  dvnmul  40796  wallispilem4  40922  wallispi2lem2  40926  stirlinglem6  40933  dirkerper  40950  dirkertrigeqlem1  40952  dirkertrigeqlem2  40953  dirkertrigeqlem3  40954  dirkercncflem1  40957  fourierdlem26  40987  fourierdlem35  40996  fourierdlem42  41003  fourierdlem51  41011  fourierdlem64  41024  fourierdlem111  41071  hoidmv1lelem2  41446  hoidmvlelem2  41450  smflimlem4  41622  deccarry  42055  sqrtpwpw2p  42126  fmtnorec2lem  42130  fmtnorec3  42136  fmtnorec4  42137  mod42tp1mod8  42195  sinhpcosh  43153
  Copyright terms: Public domain W3C validator