MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcld Unicode version

Theorem addcld 9063
Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
addcld  |-  ( ph  ->  ( A  +  B
)  e.  CC )

Proof of Theorem addcld
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addcl 9028 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721  (class class class)co 6040   CCcc 8944    + caddc 8949
This theorem is referenced by:  cnegex  9203  addcom  9208  addcomd  9224  negeu  9252  addsubass  9271  subsub2  9285  subsub4  9290  pnpcan  9296  pnncan  9298  addsub4  9300  divdir  9657  cju  9952  cnref1o  10563  xov1plusxeqvd  10997  expaddz  11379  binom3  11455  spllen  11738  crre  11874  remullem  11888  imval2  11911  cjreim2  11921  sqreulem  12118  addcn2  12342  o1add  12362  fsumadd  12487  isumadd  12506  binomlem  12563  efaddlem  12650  ef4p  12669  cosf  12681  tanval2  12689  tanval3  12690  resin4p  12694  recos4p  12695  efival  12708  sinadd  12720  cosadd  12721  tanadd  12723  sadadd2lem2  12917  sadadd2lem  12926  pythagtriplem1  13145  pythagtriplem12  13155  pythagtriplem17  13160  pcbc  13224  mul4sqlem  13276  4sqlem14  13281  vdwlem6  13309  vdwlem9  13312  mulgdirlem  14869  blcvx  18782  tchcphlem1  19145  ovollb2lem  19337  mbfadd  19506  itgcnlem  19634  itgaddlem2  19668  dvmptre  19808  dvsincos  19818  taylthlem2  20243  ptolemy  20357  tanregt0  20394  eff1olem  20403  cosargd  20456  tanarg  20467  logf1o2  20494  efopn  20502  cxpsqrlem  20546  cxpeq  20594  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  ang180lem4  20607  pythag  20612  ssscongptld  20619  chordthmlem  20626  chordthmlem2  20627  chordthmlem3  20628  chordthmlem4  20629  chordthmlem5  20630  quad2  20632  dcubic1lem  20636  dcubic2  20637  dcubic1  20638  dcubic  20639  mcubic  20640  cubic2  20641  cubic  20642  binom4  20643  dquartlem1  20644  dquartlem2  20645  dquart  20646  quart1cl  20647  quart1lem  20648  quart1  20649  quartlem1  20650  quartlem2  20651  quartlem3  20652  quartlem4  20653  quart  20654  asinlem3  20664  asinf  20665  asinneg  20679  efiasin  20681  asinsinlem  20684  asinsin  20685  asinbnd  20692  atanlogaddlem  20706  ftalem7  20814  basellem3  20818  bposlem9  21029  lgsquad2lem1  21095  dchrvmasumiflem2  21149  mulogsumlem  21178  mulog2sumlem1  21181  mulog2sumlem2  21182  mulog2sumlem3  21183  selberglem1  21192  selberg2  21198  selberg3lem1  21204  selbergr  21215  selberg3r  21216  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntrlog2bnd  21231  4ipval2  22157  4ipval3  22161  dipcj  22166  golem1  23727  lt2addrd  24068  cnre2csqima  24262  ballotlemsima  24726  dmgmaddnn0  24764  dmgmdivn0  24765  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamgulm2  24773  lgambdd  24774  lgamucov  24775  lgamcvg2  24792  gamcvg  24793  gamcvg2lem  24796  pnpncand  25160  iprodgam  25272  binomfallfaclem2  25307  brbtwn2  25748  colinearalglem1  25749  colinearalglem2  25750  axeuclidlem  25805  axcontlem2  25808  axcontlem7  25813  axcontlem8  25814  bpoly4  26009  fsumcube  26010  itg2addnclem3  26157  itgaddnclem2  26163  itgaddnc  26164  dvreasin  26179  areacirclem2  26181  areacirclem5  26185  areacirc  26187  csbrn  26346  pellexlem2  26783  pellexlem6  26787  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell14qrdich  26822  rmxyneg  26873  rmxyadd  26874  jm2.19lem4  26953  jm2.26lem3  26962  clim1fr1  27594  stoweidlem1  27617  stoweidlem11  27627  stoweidlem13  27629  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem10  27699  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem15  27704  sigaraf  27710  sigaras  27712  sinhpcosh  28197
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addcl 9006
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator