Theorem addcld 10925

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   + caddc 10805

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

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

This theorem is referenced by:  cnegex  11086  addcom  11091  addcomd  11107  muladd11r  11118  negeu  11141  addsubass  11161  subsub2  11179  subsub4  11184  pnncan  11192  addsub4  11194  pnpncand  11326  addmulsub  11367  subaddmulsub  11368  mulsubaddmulsub  11369  divdir  11588  cju  11899  cnref1o  12654  xov1plusxeqvd  13159  expaddz  13755  binom3  13867  sqoddm1div8  13886  mulsubdivbinom2  13904  muldivbinom2  13905  spllen  14395  crre  14753  remullem  14767  imval2  14790  cjreim2  14800  sqreulem  14999  bhmafibid1cn  15103  bhmafibid2cn  15104  bhmafibid1  15105  bhmafibid2  15106  addcn2  15231  o1add  15251  rlimadd  15280  fsumadd  15380  isumadd  15407  binomlem  15469  binomfallfaclem2  15678  bpoly4  15697  fsumcube  15698  efaddlem  15730  ef4p  15750  cosf  15762  tanval2  15770  tanval3  15771  resin4p  15775  recos4p  15776  efival  15789  sinadd  15801  cosadd  15802  tanadd  15804  pwp1fsum  16028  sadadd2lem2  16085  sadadd2lem  16094  pythagtriplem1  16445  pythagtriplem12  16455  pythagtriplem17  16460  pcbc  16529  mul4sqlem  16582  4sqlem14  16587  vdwlem6  16615  vdwlem9  16618  mulgdirlem  18649  blcvx  23867  cphpyth  24285  tcphcphlem1  24304  cphipval2  24310  4cphipval2  24311  csbren  24468  ovollb2lem  24557  mbfadd  24730  itgcnlem  24859  itgaddlem2  24893  dvmptre  25038  dvsincos  25050  itgpowd  25119  taylthlem2  25438  ptolemy  25558  tanregt0  25600  eff1olem  25609  cosargd  25668  tanarg  25679  logf1o2  25710  efopn  25718  cxpsqrtlem  25762  cxpeq  25815  ang180lem1  25864  ang180lem2  25865  ang180lem3  25866  ang180lem4  25867  pythag  25872  ssscongptld  25877  chordthmlem  25887  chordthmlem2  25888  chordthmlem3  25889  chordthmlem4  25890  chordthmlem5  25891  heron  25893  quad2  25894  dcubic1lem  25898  dcubic2  25899  dcubic1  25900  dcubic  25901  mcubic  25902  cubic2  25903  cubic  25904  binom4  25905  dquartlem1  25906  dquartlem2  25907  dquart  25908  quart1cl  25909  quart1lem  25910  quart1  25911  quartlem1  25912  quartlem2  25913  quartlem3  25914  quartlem4  25915  quart  25916  asinlem3  25926  asinf  25927  asinneg  25941  efiasin  25943  asinsinlem  25946  asinsin  25947  asinbnd  25954  atanlogaddlem  25968  dmgmaddnn0  26081  dmgmdivn0  26082  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem4  26086  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamgulm2  26090  lgambdd  26091  lgamucov  26092  lgamcvg2  26109  gamcvg  26110  gamcvg2lem  26113  ftalem7  26133  basellem3  26137  bposlem9  26345  lgsquad2lem1  26437  2lgslem3d1  26456  2sqmod  26489  dchrvmasumiflem2  26555  mulogsumlem  26584  mulog2sumlem1  26587  mulog2sumlem2  26588  mulog2sumlem3  26589  selberglem1  26598  selberg2  26604  selberg3lem1  26610  selbergr  26621  selberg3r  26622  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntrlog2bnd  26637  brbtwn2  27176  colinearalglem1  27177  colinearalglem2  27178  axeuclidlem  27233  axcontlem2  27236  axcontlem7  27241  axcontlem8  27242  finsumvtxdg2ssteplem4  27818  wwlksext2clwwlk  28322  4ipval2  28971  dipcj  28977  golem1  30534  lt2addrd  30976  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2  31302  archirngz  31345  archiabllem2c  31351  ccfldextdgrr  31644  cnre2csqima  31763  ballotlemsima  32382  hgt750lemb  32536  iprodgam  33614  dnizphlfeqhlf  34583  dnibndlem9  34593  knoppndvlem16  34634  itg2addnclem3  35757  itgaddnclem2  35763  itgaddnc  35764  ftc1anclem6  35782  ftc1anclem8  35784  dvasin  35788  areacirclem1  35792  areacirclem4  35795  areacirc  35797  lcmineqlem6  39970  lcmineqlem11  39975  lcmineqlem18  39982  aks4d1p1p2  40006  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  2np3bcnp1  40028  2ap1caineq  40029  sticksstones12a  40041  metakunt29  40081  mvrrsubd  40224  lsubrotld  40227  sn-negex12  40319  sn-addid1  40323  sn-subeu  40329  sn-0tie0  40342  cnreeu  40359  dffltz  40387  cu3addd  40418  3cubeslem2  40423  3cubeslem3l  40424  3cubeslem3r  40425  3cubeslem4  40427  pellexlem2  40568  pellexlem6  40572  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell14qrdich  40607  rmxyneg  40658  rmxyadd  40659  jm2.19lem4  40730  jm2.26lem3  40739  sqrtcval  41138  int-rightdistd  41680  binomcxplemnn0  41856  binomcxplemrat  41857  binomcxplemfrat  41858  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  sub2times  42702  clim1fr1  43032  limcperiod  43059  addlimc  43079  coseq0  43295  fprodaddrecnncnvlem  43340  dvxpaek  43371  dvnxpaek  43373  dvnmul  43374  itgiccshift  43411  itgperiod  43412  stoweidlem1  43432  stoweidlem11  43442  stoweidlem13  43444  wallispilem4  43499  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem15  43519  dirkerper  43527  dirkertrigeqlem1  43529  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkeritg  43533  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem18  43556  fourierdlem26  43564  fourierdlem30  43568  fourierdlem48  43585  fourierdlem49  43586  fourierdlem79  43616  fourierdlem83  43620  fourierdlem92  43629  fourierdlem93  43630  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  smfmullem1  44212  sigaraf  44256  sigaras  44258  readdcnnred  44683  fmtnorec4  44889  quad1  44960  requad01  44961  requad2  44963  fldivmod  45752  dignn0flhalflem1  45849  affinecomb2  45937  eenglngeehlnmlem1  45971  itschlc0yqe  45994  itsclc0yqsollem1  45996  itsclc0yqsol  45998  itscnhlc0xyqsol  45999  itsclc0xyqsolr  46003  2itscplem3  46014  itscnhlinecirc02plem1  46016  inlinecirc02plem  46020  sinhpcosh  46328