Theorem addassd 11166

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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		addass 11125	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
5	1, 2, 3, 4	syl3anc 1374	1 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  addrid  11325  cnegex  11326  addlid  11328  addcan  11329  addcan2  11330  addcom  11331  addcomd  11347  muladd11r  11358  negeu  11382  addsubass  11402  nppcan3  11417  addsubsub23  11557  muladd  11581  add1p1  12404  div4p1lem1div2  12408  zpnn0elfzo1  13667  flhalf  13762  fldiv  13792  binom3  14159  bernneq  14164  discr1  14174  ccatass  14524  cshweqrep  14756  01sqrexlem7  15183  sqreulem  15295  isercoll2  15604  caucvgrlem  15608  iseraltlem2  15618  bcxmas  15770  bpoly4  15994  efsep  16047  efi4p  16074  efival  16089  pwp1fsum  16330  flodddiv4  16354  sadadd2lem2  16389  sadadd2lem  16398  sadasslem  16409  pcadd2  16830  prmreclem6  16861  4sqlem11  16895  vdwapun  16914  vdwlem3  16923  vdwlem6  16926  vdwlem8  16928  vdwlem9  16929  prmgaplem8  16998  psgnunilem2  19436  sylow1lem1  19539  efgredlemc  19686  psdmul  22121  opnreen  24788  ovolunlem1a  25465  nulmbl2  25505  unmbl  25506  volinun  25515  uniioombllem5  25556  itgcnlem  25759  ditgsplit  25830  dvnadd  25899  dvntaylp  26347  ulmshft  26367  ulmcn  26376  tangtx  26482  heron  26816  quad2  26817  dcubic1lem  26821  mcubic  26825  binom4  26828  dquartlem1  26829  dquartlem2  26830  dquart  26831  quart1  26834  quart  26839  lgamcvg2  27033  basellem2  27060  basellem3  27061  basellem8  27066  ppiub  27183  bcp1ctr  27258  bposlem9  27271  2lgslem3c  27377  2lgslem3d  27378  selberg3  27538  pntpbnd2  27566  pntibndlem2  27570  pntlemg  27577  pntlemk  27585  pntlemo  27586  axeuclidlem  29047  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  finsumvtxdg2ssteplem4  29634  wwlksnextwrd  29982  wwlksnextproplem3  29996  wwlksext2clwwlk  30144  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  smcnlem  30784  stadd3i  32335  golem1  32358  quad3d  32839  cycpmco2lem3  33221  cycpmco2lem4  33222  cycpmco2lem5  33223  cycpmco2lem6  33224  cycpmco2  33226  archirngz  33282  constrrtlc1  33909  constrrtcclem  33911  constrrtcc  33912  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  subfacval2  35400  subfaclim  35401  subfacval3  35402  faclimlem1  35956  faclim2  35961  fwddifnp1  36378  dnizphlfeqhlf  36695  dnibndlem10  36706  dnibndlem13  36709  poimirlem16  37881  itg2addnclem3  37918  itg2addnc  37919  areacirclem1  37953  aks4d1p1p2  42434  posbezout  42464  2np3bcnp1  42508  sticksstones12a  42521  bcle2d  42543  aks6d1c7lem1  42544  readdridaddlidd  42622  nnadd1com  42631  nnaddcom  42632  nnadddir  42634  resubeulem1  42739  resubeulem2  42740  readdsub  42748  resubsub4  42753  resubidaddlidlem  42758  sn-addlid  42768  renegneg  42776  readdcan2  42777  renegid2  42778  sn-it0e0  42780  sn-negex12  42781  sn-addcand  42784  sn-addrid  42785  sn-addcan2d  42786  sn-subeu  42791  sn-0tie0  42815  zaddcomlem  42827  zaddcom  42828  cnreeu  42854  dffltz  42986  3cubeslem2  43036  3cubeslem3l  43037  3cubeslem3r  43038  jm2.19lem3  43342  jm2.25  43350  int-addassocd  44524  binomcxplemnotnn0  44706  sub2times  45629  fperiodmullem  45659  dvnmul  46295  wallispilem4  46420  wallispi2lem2  46424  stirlinglem6  46431  dirkerper  46448  dirkertrigeqlem1  46450  dirkertrigeqlem2  46451  dirkertrigeqlem3  46452  dirkercncflem1  46455  fourierdlem26  46485  fourierdlem35  46494  fourierdlem42  46501  fourierdlem51  46509  fourierdlem64  46522  fourierdlem111  46569  hoidmv1lelem2  46944  hoidmvlelem2  46948  smflimlem4  47126  deccarry  47665  sqrtpwpw2p  47892  fmtnorec2lem  47896  fmtnorec3  47902  fmtnorec4  47903  mod42tp1mod8  47956  gpg5nbgrvtx13starlem2  48426  itcovalpclem2  49025  ackval1  49035  ackval2  49036  itscnhlc0yqe  49113  itsclquadb  49130  sinhpcosh  50093