Theorem addcld 11215

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 11174	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7393  ℂcc 11090   + caddc 11095

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

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  cnegex  11377  addcom  11382  addcomd  11398  muladd11r  11409  negeu  11432  addsubass  11452  subsub2  11470  subsub4  11475  pnncan  11483  addsub4  11485  pnpncand  11617  addmulsub  11658  subaddmulsub  11659  mulsubaddmulsub  11660  divdir  11879  cju  12190  cnref1o  12951  xov1plusxeqvd  13457  expaddz  14054  binom3  14169  sqoddm1div8  14188  mulsubdivbinom2  14204  muldivbinom2  14205  spllen  14686  crre  15043  remullem  15057  imval2  15080  cjreim2  15090  sqreulem  15288  bhmafibid1cn  15392  bhmafibid2cn  15393  bhmafibid1  15394  bhmafibid2  15395  addcn2  15520  o1add  15540  rlimadd  15569  fsumadd  15668  isumadd  15695  binomlem  15757  binomfallfaclem2  15966  bpoly4  15985  fsumcube  15986  efaddlem  16018  ef4p  16038  cosf  16050  tanval2  16058  tanval3  16059  resin4p  16063  recos4p  16064  efival  16077  sinadd  16089  cosadd  16090  tanadd  16092  pwp1fsum  16316  sadadd2lem2  16373  sadadd2lem  16382  pythagtriplem1  16731  pythagtriplem12  16741  pythagtriplem17  16746  pcbc  16815  mul4sqlem  16868  4sqlem14  16873  vdwlem6  16901  vdwlem9  16904  mulgdirlem  18957  blcvx  24243  cphpyth  24662  tcphcphlem1  24681  cphipval2  24687  4cphipval2  24688  csbren  24845  ovollb2lem  24934  mbfadd  25107  itgcnlem  25236  itgaddlem2  25270  dvmptre  25415  dvsincos  25427  itgpowd  25496  taylthlem2  25815  ptolemy  25935  tanregt0  25977  eff1olem  25986  cosargd  26045  tanarg  26056  logf1o2  26087  efopn  26095  cxpsqrtlem  26139  cxpeq  26192  ang180lem1  26241  ang180lem2  26242  ang180lem3  26243  ang180lem4  26244  pythag  26249  ssscongptld  26254  chordthmlem  26264  chordthmlem2  26265  chordthmlem3  26266  chordthmlem4  26267  chordthmlem5  26268  heron  26270  quad2  26271  dcubic1lem  26275  dcubic2  26276  dcubic1  26277  dcubic  26278  mcubic  26279  cubic2  26280  cubic  26281  binom4  26282  dquartlem1  26283  dquartlem2  26284  dquart  26285  quart1cl  26286  quart1lem  26287  quart1  26288  quartlem1  26289  quartlem2  26290  quartlem3  26291  quartlem4  26292  quart  26293  asinlem3  26303  asinf  26304  asinneg  26318  efiasin  26320  asinsinlem  26323  asinsin  26324  asinbnd  26331  atanlogaddlem  26345  dmgmaddnn0  26458  dmgmdivn0  26459  lgamgulmlem2  26461  lgamgulmlem3  26462  lgamgulmlem4  26463  lgamgulmlem5  26464  lgamgulmlem6  26465  lgamgulm2  26467  lgambdd  26468  lgamucov  26469  lgamcvg2  26486  gamcvg  26487  gamcvg2lem  26490  ftalem7  26510  basellem3  26514  bposlem9  26722  lgsquad2lem1  26814  2lgslem3d1  26833  2sqmod  26866  dchrvmasumiflem2  26932  mulogsumlem  26961  mulog2sumlem1  26964  mulog2sumlem2  26965  mulog2sumlem3  26966  selberglem1  26975  selberg2  26981  selberg3lem1  26987  selbergr  26998  selberg3r  26999  pntrlog2bndlem1  27007  pntrlog2bndlem2  27008  pntrlog2bndlem5  27011  pntrlog2bndlem6  27013  pntrlog2bnd  27014  brbtwn2  28028  colinearalglem1  28029  colinearalglem2  28030  axeuclidlem  28085  axcontlem2  28088  axcontlem7  28093  axcontlem8  28094  finsumvtxdg2ssteplem4  28670  wwlksext2clwwlk  29175  4ipval2  29824  dipcj  29830  golem1  31387  lt2addrd  31835  cycpmco2lem3  32158  cycpmco2lem4  32159  cycpmco2lem5  32160  cycpmco2lem6  32161  cycpmco2  32163  archirngz  32206  archiabllem2c  32212  ccfldextdgrr  32584  cnre2csqima  32722  ballotlemsima  33345  hgt750lemb  33499  iprodgam  34542  dnizphlfeqhlf  35156  dnibndlem9  35166  knoppndvlem16  35207  itg2addnclem3  36345  itgaddnclem2  36351  itgaddnc  36352  ftc1anclem6  36370  ftc1anclem8  36372  dvasin  36376  areacirclem1  36380  areacirclem4  36383  areacirc  36385  lcmineqlem6  40704  lcmineqlem11  40709  lcmineqlem18  40716  aks4d1p1p2  40740  aks4d1p1p6  40743  aks4d1p1p7  40744  aks4d1p1p5  40745  2np3bcnp1  40765  2ap1caineq  40766  sticksstones12a  40778  metakunt29  40818  mvrrsubd  40975  lsubrotld  40978  sn-negex12  41071  sn-addrid  41075  sn-subeu  41081  sn-0tie0  41094  zaddcomlem  41106  zaddcom  41107  cnreeu  41123  dffltz  41158  cu3addd  41189  3cubeslem2  41194  3cubeslem3l  41195  3cubeslem3r  41196  3cubeslem4  41198  pellexlem2  41339  pellexlem6  41343  pell1234qrreccl  41363  pell1234qrmulcl  41364  pell14qrdich  41378  rmxyneg  41430  rmxyadd  41431  jm2.19lem4  41502  jm2.26lem3  41511  sqrtcval  42163  int-rightdistd  42703  binomcxplemnn0  42879  binomcxplemrat  42880  binomcxplemfrat  42881  binomcxplemdvbinom  42883  binomcxplemnotnn0  42886  sub2times  43755  clim1fr1  44090  limcperiod  44117  addlimc  44137  coseq0  44353  fprodaddrecnncnvlem  44398  dvxpaek  44429  dvnxpaek  44431  dvnmul  44432  itgiccshift  44469  itgperiod  44470  stoweidlem1  44490  stoweidlem11  44500  stoweidlem13  44502  wallispilem4  44557  wallispilem5  44558  wallispi  44559  wallispi2lem1  44560  wallispi2lem2  44561  wallispi2  44562  stirlinglem1  44563  stirlinglem3  44565  stirlinglem4  44566  stirlinglem5  44567  stirlinglem6  44568  stirlinglem7  44569  stirlinglem10  44572  stirlinglem11  44573  stirlinglem12  44574  stirlinglem13  44575  stirlinglem15  44577  dirkerper  44585  dirkertrigeqlem1  44587  dirkertrigeqlem2  44588  dirkertrigeqlem3  44589  dirkeritg  44591  dirkercncflem2  44593  dirkercncflem4  44595  fourierdlem18  44614  fourierdlem26  44622  fourierdlem30  44626  fourierdlem48  44643  fourierdlem49  44644  fourierdlem79  44674  fourierdlem83  44678  fourierdlem92  44687  fourierdlem93  44688  fourierdlem103  44698  fourierdlem104  44699  fourierdlem111  44706  fourierdlem112  44707  smfmullem1  45280  sigaraf  45342  sigaras  45344  readdcnnred  45783  fmtnorec4  45989  quad1  46060  requad01  46061  requad2  46063  fldivmod  46852  dignn0flhalflem1  46949  affinecomb2  47037  eenglngeehlnmlem1  47071  itschlc0yqe  47094  itsclc0yqsollem1  47096  itsclc0yqsol  47098  itscnhlc0xyqsol  47099  itsclc0xyqsolr  47103  2itscplem3  47114  itscnhlinecirc02plem1  47116  inlinecirc02plem  47120  sinhpcosh  47433