Theorem addcld 7914

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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		addcld.2	. 2 |- ( ph -> B e. CC )
3		addcl 7874	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
4	1, 2, 3	syl2anc 409	1 |- ( ph -> ( A + B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 2136  (class class class)co 5841   CCcc 7747   + caddc 7752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-addcl 7845

This theorem is referenced by:  muladd11r  8050  negeu  8085  addsubass  8104  subsub2  8122  subsub4  8127  pnpcan  8133  pnncan  8135  addsub4  8137  pnpncand  8269  apreim  8497  addext  8504  aprcl  8540  divdirap  8589  recp1lt1  8790  cju  8852  cnref1o  9584  modsumfzodifsn  10327  expaddzap  10495  binom2  10562  binom3  10568  sqoddm1div8  10604  nn0opthlem1d  10629  reval  10787  imval  10788  crre  10795  remullem  10809  imval2  10832  cjreim2  10842  cnrecnv  10848  resqrexlemcalc1  10952  maxabslemab  11144  maxltsup  11156  max0addsup  11157  minabs  11173  bdtrilem  11176  bdtri  11177  addcn2  11247  fsumadd  11343  isumadd  11368  binomlem  11420  efaddlem  11611  ef4p  11631  cosval  11640  cosf  11642  tanval2ap  11650  tanval3ap  11651  resin4p  11655  recos4p  11656  efival  11669  sinadd  11673  cosadd  11674  tanaddap  11676  pythagtriplem1  12193  pythagtriplem12  12203  pythagtriplem16  12207  pythagtriplem17  12208  pcbc  12277  mul4sqlem  12319  oddennn  12321  addccncf  13186  limcimolemlt  13233  dvaddxxbr  13265  ptolemy  13345  rpcxpadd  13426  binom4  13497  qdencn  13866  iooref1o  13873  apdifflemr  13886