Theorem addcld 11231

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

Syntax hints:   → wi 4   ∈ wcel 2150  (class class class)co 7414  ℂcc 11101   + caddc 11106

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

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

This theorem is referenced by:  cnegex  11394  addcom  11399  addcomd  11415  muladd11r  11426  negeu  11450  addsubass  11470  subsub2  11489  subsub4  11494  pnncan  11502  addsub4  11504  addsubsub23  11625  pnpncand  11638  addmulsub  11679  subaddmulsub  11680  mulsubaddmulsub  11681  divdir  11900  cju  12217  cnref1o  13012  xov1plusxeqvd  13528  modaddb  13945  expaddz  14145  binom3  14263  sqoddm1div8  14282  mulsubdivbinom2  14301  muldivbinom2  14302  spllen  14794  crre  15168  remullem  15182  imval2  15205  cjreim2  15215  sqreulem  15414  bhmafibid1cn  15520  bhmafibid2cn  15521  bhmafibid1  15522  bhmafibid2  15523  addcn2  15648  o1add  15668  rlimadd  15697  fsumadd  15794  isumadd  15821  binomlem  15886  binomfallfaclem2  16097  bpoly4  16116  fsumcube  16117  efaddlem  16150  ef4p  16172  cosf  16184  tanval2  16192  tanval3  16193  resin4p  16197  recos4p  16198  efival  16211  sinadd  16223  cosadd  16224  tanadd  16226  pwp1fsum  16452  sadadd2lem2  16511  sadadd2lem  16520  pythagtriplem1  16879  pythagtriplem12  16889  pythagtriplem17  16894  pcbc  16963  mul4sqlem  17016  4sqlem14  17021  vdwlem6  17049  vdwlem9  17052  mulgdirlem  19174  blcvx  24938  cphpyth  25358  tcphcphlem1  25377  cphipval2  25383  4cphipval2  25384  csbren  25541  ovollb2lem  25630  mbfadd  25803  itgcnlem  25932  itgaddlem2  25966  dvmptre  26111  dvsincos  26123  itgpowd  26192  taylthlem2  26517  ptolemy  26641  tanregt0  26684  eff1olem  26693  cosargd  26753  tanarg  26764  logf1o2  26795  efopn  26803  cxpsqrtlem  26847  cxpeq  26902  ang180lem1  26954  ang180lem2  26955  ang180lem3  26956  ang180lem4  26957  pythag  26962  ssscongptld  26967  chordthmlem  26977  chordthmlem2  26978  chordthmlem3  26979  chordthmlem4  26980  chordthmlem5  26981  heron  26983  quad2  26984  dcubic1lem  26988  dcubic2  26989  dcubic1  26990  dcubic  26991  mcubic  26992  cubic2  26993  cubic  26994  binom4  26995  dquartlem1  26996  dquartlem2  26997  dquart  26998  quart1cl  26999  quart1lem  27000  quart1  27001  quartlem1  27002  quartlem2  27003  quartlem3  27004  quartlem4  27005  quart  27006  asinlem3  27016  asinf  27017  asinneg  27031  efiasin  27033  asinsinlem  27036  asinsin  27037  asinbnd  27044  atanlogaddlem  27058  dmgmaddnn0  27171  dmgmdivn0  27172  lgamgulmlem2  27174  lgamgulmlem3  27175  lgamgulmlem4  27176  lgamgulmlem5  27177  lgamgulmlem6  27178  lgamgulm2  27180  lgambdd  27181  lgamucov  27182  lgamcvg2  27199  gamcvg  27200  gamcvg2lem  27203  ftalem7  27223  basellem3  27227  bposlem9  27436  lgsquad2lem1  27528  2lgslem3d1  27547  2sqmod  27580  dchrvmasumiflem2  27646  mulogsumlem  27675  mulog2sumlem1  27678  mulog2sumlem2  27679  mulog2sumlem3  27680  selberglem1  27689  selberg2  27695  selberg3lem1  27701  selbergr  27712  selberg3r  27713  pntrlog2bndlem1  27721  pntrlog2bndlem2  27722  pntrlog2bndlem5  27725  pntrlog2bndlem6  27727  pntrlog2bnd  27728  brbtwn2  29225  colinearalglem1  29226  colinearalglem2  29227  axeuclidlem  29282  axcontlem2  29285  axcontlem7  29290  axcontlem8  29291  finsumvtxdg2ssteplem4  29868  wwlksext2clwwlk  30378  4ipval2  31030  dipcj  31036  golem1  32593  submuladdd  33055  binom2subadd  33056  pythagreim  33060  quad3d  33064  lt2addrd  33065  cycpmco2lem3  33418  cycpmco2lem4  33419  cycpmco2lem5  33420  cycpmco2lem6  33421  cycpmco2  33423  archirngz  33479  archiabllem2c  33485  zringfrac  33814  ccfldextdgrr  34032  constrrtll  34091  constrrtlc1  34092  constrrtcclem  34094  constrrtcc  34095  constrfin  34106  nn0constr  34121  constraddcl  34122  constrrecl  34129  constrresqrtcl  34137  constrsqrtcl  34139  cos9thpiminplylem1  34142  cos9thpiminplylem2  34143  cos9thpiminplylem3  34144  cos9thpiminply  34148  cos9thpinconstrlem1  34149  cos9thpinconstrlem2  34150  cnre2csqima  34271  ballotlemsima  34876  hgt750lemb  35013  iprodgam  36192  dnizphlfeqhlf  37013  dnibndlem9  37023  knoppndvlem16  37064  qdiff  37919  itg2addnclem3  38272  itgaddnclem2  38278  itgaddnc  38279  ftc1anclem6  38297  ftc1anclem8  38299  dvasin  38303  areacirclem1  38307  areacirclem4  38310  areacirc  38312  lcmineqlem6  42751  lcmineqlem11  42756  lcmineqlem18  42763  aks4d1p1p2  42787  aks4d1p1p6  42790  aks4d1p1p7  42791  aks4d1p1p5  42792  posbezout  42817  2np3bcnp1  42861  2ap1caineq  42862  sticksstones12a  42874  bcle2d  42896  quadfac  42922  mvrrsubd  42985  lsubrotld  42988  oddnumth  43022  sumcubes  43024  cxp112d  43052  cxp111d  43053  sn-negex12  43128  sn-addrid  43132  sn-subeu  43138  sn-0tie0  43175  zaddcomlem  43187  zaddcom  43188  cnreeu  43214  dffltz  43318  cu3addd  43364  3cubeslem2  43368  3cubeslem3l  43369  3cubeslem3r  43370  3cubeslem4  43372  pellexlem2  43509  pellexlem6  43513  pell1234qrreccl  43533  pell1234qrmulcl  43534  pell14qrdich  43548  rmxyneg  43599  rmxyadd  43600  jm2.19lem4  43671  jm2.26lem3  43680  sqrtcval  44319  int-rightdistd  44858  binomcxplemnn0  45011  binomcxplemrat  45012  binomcxplemfrat  45013  binomcxplemdvbinom  45015  binomcxplemnotnn0  45018  sub2times  45944  clim1fr1  46269  limcperiod  46296  addlimc  46314  coseq0  46530  fprodaddrecnncnvlem  46575  dvxpaek  46606  dvnxpaek  46608  dvnmul  46609  itgiccshift  46646  itgperiod  46647  stoweidlem1  46667  stoweidlem11  46677  stoweidlem13  46679  wallispilem4  46734  wallispilem5  46735  wallispi  46736  wallispi2lem1  46737  wallispi2lem2  46738  wallispi2  46739  stirlinglem1  46740  stirlinglem3  46742  stirlinglem4  46743  stirlinglem5  46744  stirlinglem6  46745  stirlinglem7  46746  stirlinglem10  46749  stirlinglem11  46750  stirlinglem12  46751  stirlinglem13  46752  stirlinglem15  46754  dirkerper  46762  dirkertrigeqlem1  46764  dirkertrigeqlem2  46765  dirkertrigeqlem3  46766  dirkeritg  46768  dirkercncflem2  46770  dirkercncflem4  46772  fourierdlem18  46791  fourierdlem26  46799  fourierdlem30  46803  fourierdlem48  46820  fourierdlem49  46821  fourierdlem79  46851  fourierdlem83  46855  fourierdlem92  46864  fourierdlem93  46865  fourierdlem103  46875  fourierdlem104  46876  fourierdlem111  46883  fourierdlem112  46884  smfmullem1  47457  sigaraf  47519  sigaras  47521  sin5tlem1  47559  sin5tlem4  47562  sin5tlem5  47563  readdcnnred  47989  fldivmod  48030  fmtnorec4  48250  quad1  48334  requad01  48335  requad2  48337  gpgedgvtx1  48776  dignn0flhalflem1  49344  affinecomb2  49432  eenglngeehlnmlem1  49466  itschlc0yqe  49489  itsclc0yqsollem1  49491  itsclc0yqsol  49493  itscnhlc0xyqsol  49494  itsclc0xyqsolr  49498  2itscplem3  49509  itscnhlinecirc02plem1  49511  inlinecirc02plem  49515  sinhpcosh  50467