Theorem addcld 10699

Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
addcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcl 10658	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 588	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2112  (class class class)co 7151  ℂcc 10574   + caddc 10579

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  cnegex  10860  addcom  10865  addcomd  10881  muladd11r  10892  negeu  10915  addsubass  10935  subsub2  10953  subsub4  10958  pnncan  10966  addsub4  10968  pnpncand  11100  addmulsub  11141  subaddmulsub  11142  mulsubaddmulsub  11143  divdir  11362  cju  11671  cnref1o  12426  xov1plusxeqvd  12931  expaddz  13524  binom3  13636  sqoddm1div8  13655  mulsubdivbinom2  13673  muldivbinom2  13674  spllen  14164  crre  14522  remullem  14536  imval2  14559  cjreim2  14569  sqreulem  14768  bhmafibid1cn  14872  bhmafibid2cn  14873  bhmafibid1  14874  bhmafibid2  14875  addcn2  14999  o1add  15019  fsumadd  15145  isumadd  15171  binomlem  15233  binomfallfaclem2  15443  bpoly4  15462  fsumcube  15463  efaddlem  15495  ef4p  15515  cosf  15527  tanval2  15535  tanval3  15536  resin4p  15540  recos4p  15541  efival  15554  sinadd  15566  cosadd  15567  tanadd  15569  pwp1fsum  15793  sadadd2lem2  15850  sadadd2lem  15859  pythagtriplem1  16209  pythagtriplem12  16219  pythagtriplem17  16224  pcbc  16292  mul4sqlem  16345  4sqlem14  16350  vdwlem6  16378  vdwlem9  16381  mulgdirlem  18326  blcvx  23500  tcphcphlem1  23936  cphipval2  23942  4cphipval2  23943  csbren  24100  ovollb2lem  24189  mbfadd  24362  itgcnlem  24490  itgaddlem2  24524  dvmptre  24669  dvsincos  24681  itgpowd  24750  taylthlem2  25069  ptolemy  25189  tanregt0  25231  eff1olem  25240  cosargd  25299  tanarg  25310  logf1o2  25341  efopn  25349  cxpsqrtlem  25393  cxpeq  25446  ang180lem1  25495  ang180lem2  25496  ang180lem3  25497  ang180lem4  25498  pythag  25503  ssscongptld  25508  chordthmlem  25518  chordthmlem2  25519  chordthmlem3  25520  chordthmlem4  25521  chordthmlem5  25522  heron  25524  quad2  25525  dcubic1lem  25529  dcubic2  25530  dcubic1  25531  dcubic  25532  mcubic  25533  cubic2  25534  cubic  25535  binom4  25536  dquartlem1  25537  dquartlem2  25538  dquart  25539  quart1cl  25540  quart1lem  25541  quart1  25542  quartlem1  25543  quartlem2  25544  quartlem3  25545  quartlem4  25546  quart  25547  asinlem3  25557  asinf  25558  asinneg  25572  efiasin  25574  asinsinlem  25577  asinsin  25578  asinbnd  25585  atanlogaddlem  25599  dmgmaddnn0  25712  dmgmdivn0  25713  lgamgulmlem2  25715  lgamgulmlem3  25716  lgamgulmlem4  25717  lgamgulmlem5  25718  lgamgulmlem6  25719  lgamgulm2  25721  lgambdd  25722  lgamucov  25723  lgamcvg2  25740  gamcvg  25741  gamcvg2lem  25744  ftalem7  25764  basellem3  25768  bposlem9  25976  lgsquad2lem1  26068  2lgslem3d1  26087  2sqmod  26120  dchrvmasumiflem2  26186  mulogsumlem  26215  mulog2sumlem1  26218  mulog2sumlem2  26219  mulog2sumlem3  26220  selberglem1  26229  selberg2  26235  selberg3lem1  26241  selbergr  26252  selberg3r  26253  pntrlog2bndlem1  26261  pntrlog2bndlem2  26262  pntrlog2bndlem5  26265  pntrlog2bndlem6  26267  pntrlog2bnd  26268  brbtwn2  26799  colinearalglem1  26800  colinearalglem2  26801  axeuclidlem  26856  axcontlem2  26859  axcontlem7  26864  axcontlem8  26865  finsumvtxdg2ssteplem4  27438  wwlksext2clwwlk  27942  4ipval2  28591  dipcj  28597  golem1  30154  lt2addrd  30599  cycpmco2lem3  30922  cycpmco2lem4  30923  cycpmco2lem5  30924  cycpmco2lem6  30925  cycpmco2  30927  archirngz  30970  archiabllem2c  30976  ccfldextdgrr  31264  cnre2csqima  31383  ballotlemsima  32002  hgt750lemb  32156  iprodgam  33224  dnizphlfeqhlf  34206  dnibndlem9  34216  knoppndvlem16  34257  itg2addnclem3  35391  itgaddnclem2  35397  itgaddnc  35398  ftc1anclem6  35416  ftc1anclem8  35418  dvasin  35422  areacirclem1  35426  areacirclem4  35429  areacirc  35431  lcmineqlem6  39602  lcmineqlem11  39607  lcmineqlem18  39614  aks4d1p1p2  39637  aks4d1p1p6  39640  aks4d1p1p7  39641  aks4d1p1p5  39642  2np3bcnp1  39646  2ap1caineq  39647  metakunt29  39676  mvrrsubd  39806  lsubrotld  39809  sn-negex12  39896  sn-addid1  39900  sn-subeu  39906  sn-0tie0  39919  cnreeu  39936  dffltz  39964  cu3addd  39995  3cubeslem2  40000  3cubeslem3l  40001  3cubeslem3r  40002  3cubeslem4  40004  pellexlem2  40145  pellexlem6  40149  pell1234qrreccl  40169  pell1234qrmulcl  40170  pell14qrdich  40184  rmxyneg  40235  rmxyadd  40236  jm2.19lem4  40307  jm2.26lem3  40316  sqrtcval  40715  int-rightdistd  41260  binomcxplemnn0  41427  binomcxplemrat  41428  binomcxplemfrat  41429  binomcxplemdvbinom  41431  binomcxplemnotnn0  41434  sub2times  42274  clim1fr1  42610  limcperiod  42637  addlimc  42657  coseq0  42873  fprodaddrecnncnvlem  42918  dvxpaek  42949  dvnxpaek  42951  dvnmul  42952  itgiccshift  42989  itgperiod  42990  stoweidlem1  43010  stoweidlem11  43020  stoweidlem13  43022  wallispilem4  43077  wallispilem5  43078  wallispi  43079  wallispi2lem1  43080  wallispi2lem2  43081  wallispi2  43082  stirlinglem1  43083  stirlinglem3  43085  stirlinglem4  43086  stirlinglem5  43087  stirlinglem6  43088  stirlinglem7  43089  stirlinglem10  43092  stirlinglem11  43093  stirlinglem12  43094  stirlinglem13  43095  stirlinglem15  43097  dirkerper  43105  dirkertrigeqlem1  43107  dirkertrigeqlem2  43108  dirkertrigeqlem3  43109  dirkeritg  43111  dirkercncflem2  43113  dirkercncflem4  43115  fourierdlem18  43134  fourierdlem26  43142  fourierdlem30  43146  fourierdlem48  43163  fourierdlem49  43164  fourierdlem79  43194  fourierdlem83  43198  fourierdlem92  43207  fourierdlem93  43208  fourierdlem103  43218  fourierdlem104  43219  fourierdlem111  43226  fourierdlem112  43227  smfmullem1  43790  sigaraf  43834  sigaras  43836  readdcnnred  44229  fmtnorec4  44435  quad1  44506  requad01  44507  requad2  44509  fldivmod  45298  dignn0flhalflem1  45395  affinecomb2  45483  eenglngeehlnmlem1  45517  itschlc0yqe  45540  itsclc0yqsollem1  45542  itsclc0yqsol  45544  itscnhlc0xyqsol  45545  itsclc0xyqsolr  45549  2itscplem3  45560  itscnhlinecirc02plem1  45562  inlinecirc02plem  45566  sinhpcosh  45658