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

Theorem addassd 10274
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 10235 . 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 6814  cc 10146   + caddc 10151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 10213
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074
This theorem is referenced by:  addid1  10428  cnegex  10429  addid2  10431  addcan  10432  addcan2  10433  addcom  10434  addcomd  10450  muladd11r  10461  negeu  10483  addsubass  10503  nppcan3  10517  muladd  10674  add1p1  11495  div4p1lem1div2  11499  zpnn0elfzo1  12756  flhalf  12845  fldiv  12873  binom3  13199  bernneq  13204  discr1  13214  ccatass  13580  cshweqrep  13787  sqrlem7  14208  sqreulem  14318  isercoll2  14618  caucvgrlem  14622  iseraltlem2  14632  bcxmas  14786  bpoly4  15009  efsep  15059  efi4p  15086  efival  15101  pwp1fsum  15336  flodddiv4  15359  sadadd2lem2  15394  sadadd2lem  15403  sadasslem  15414  pcadd2  15816  prmreclem6  15847  4sqlem11  15881  vdwapun  15900  vdwlem3  15909  vdwlem6  15912  vdwlem8  15914  vdwlem9  15915  prmgaplem8  15984  psgnunilem2  18135  sylow1lem1  18233  efgredlemc  18378  opnreen  22855  ovolunlem1a  23484  nulmbl2  23524  unmbl  23525  volinun  23534  uniioombllem5  23575  itgcnlem  23775  ditgsplit  23844  dvnadd  23911  dvntaylp  24344  ulmshft  24363  ulmcn  24372  tangtx  24477  heron  24785  quad2  24786  dcubic1lem  24790  mcubic  24794  binom4  24797  dquartlem1  24798  dquartlem2  24799  dquart  24800  quart1  24803  quart  24808  lgamcvg2  25001  basellem2  25028  basellem3  25029  basellem8  25034  ppiub  25149  bcp1ctr  25224  bposlem9  25237  2lgslem3c  25343  2lgslem3d  25344  selberg3  25468  pntpbnd2  25496  pntibndlem2  25500  pntlemg  25507  pntlemk  25515  pntlemo  25516  axeuclidlem  26062  axcontlem2  26065  axcontlem4  26067  axcontlem7  26070  finsumvtxdg2ssteplem4  26675  wwlksnextwrd  27036  wwlksnextproplem3  27050  wwlksext2clwwlk  27208  wwlksext2clwwlkOLD  27209  numclwlk2lem2f  27559  numclwlk2lem2f1o  27561  numclwlk2lem2fOLD  27566  numclwlk2lem2f1oOLD  27568  smcnlem  27882  stadd3i  29437  golem1  29460  archirngz  30073  subfacval2  31497  subfaclim  31498  subfacval3  31499  faclimlem1  31957  faclim2  31962  fwddifnp1  32599  dnizphlfeqhlf  32793  dnibndlem10  32804  dnibndlem13  32807  poimirlem16  33756  itg2addnclem3  33794  itg2addnc  33795  areacirclem1  33831  jm2.19lem3  38078  jm2.25  38086  int-addassocd  38997  binomcxplemnotnn0  39075  sub2times  40002  fperiodmullem  40034  dvnmul  40679  wallispilem4  40806  wallispi2lem2  40810  stirlinglem6  40817  dirkerper  40834  dirkertrigeqlem1  40836  dirkertrigeqlem2  40837  dirkertrigeqlem3  40838  dirkercncflem1  40841  fourierdlem26  40871  fourierdlem35  40880  fourierdlem42  40887  fourierdlem51  40895  fourierdlem64  40908  fourierdlem111  40955  hoidmv1lelem2  41330  hoidmvlelem2  41334  smflimlem4  41506  deccarry  41849  sqrtpwpw2p  41978  fmtnorec2lem  41982  fmtnorec3  41988  fmtnorec4  41989  mod42tp1mod8  42047  sinhpcosh  43012
  Copyright terms: Public domain W3C validator