Theorem addcld 7939

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 7899	. 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 2141  (class class class)co 5853   CCcc 7772   + caddc 7777

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

This theorem is referenced by:  muladd11r  8075  negeu  8110  addsubass  8129  subsub2  8147  subsub4  8152  pnpcan  8158  pnncan  8160  addsub4  8162  pnpncand  8294  apreim  8522  addext  8529  aprcl  8565  divdirap  8614  recp1lt1  8815  cju  8877  cnref1o  9609  modsumfzodifsn  10352  expaddzap  10520  binom2  10587  binom3  10593  sqoddm1div8  10629  nn0opthlem1d  10654  reval  10813  imval  10814  crre  10821  remullem  10835  imval2  10858  cjreim2  10868  cnrecnv  10874  resqrexlemcalc1  10978  maxabslemab  11170  maxltsup  11182  max0addsup  11183  minabs  11199  bdtrilem  11202  bdtri  11203  addcn2  11273  fsumadd  11369  isumadd  11394  binomlem  11446  efaddlem  11637  ef4p  11657  cosval  11666  cosf  11668  tanval2ap  11676  tanval3ap  11677  resin4p  11681  recos4p  11682  efival  11695  sinadd  11699  cosadd  11700  tanaddap  11702  pythagtriplem1  12219  pythagtriplem12  12229  pythagtriplem16  12233  pythagtriplem17  12234  pcbc  12303  mul4sqlem  12345  oddennn  12347  addccncf  13380  limcimolemlt  13427  dvaddxxbr  13459  ptolemy  13539  rpcxpadd  13620  binom4  13691  qdencn  14059  iooref1o  14066  apdifflemr  14079