Theorem addcld 8092

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 8050	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A + B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 2176  (class class class)co 5944   CCcc 7923   + caddc 7928

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

This theorem is referenced by:  muladd11r  8228  negeu  8263  addsubass  8282  subsub2  8300  subsub4  8305  pnpcan  8311  pnncan  8313  addsub4  8315  pnpncand  8447  apreim  8676  addext  8683  aprcl  8719  aptap  8723  divdirap  8770  recp1lt1  8972  cju  9034  cnref1o  9772  modsumfzodifsn  10541  expaddzap  10728  binom2  10796  binom3  10802  sqoddm1div8  10838  mulsubdivbinom2ap  10856  nn0opthlem1d  10865  reval  11160  imval  11161  crre  11168  remullem  11182  imval2  11205  cjreim2  11215  cnrecnv  11221  resqrexlemcalc1  11325  maxabslemab  11517  maxltsup  11529  max0addsup  11530  minabs  11547  bdtrilem  11550  bdtri  11551  addcn2  11621  fsumadd  11717  isumadd  11742  binomlem  11794  efaddlem  11985  ef4p  12005  cosval  12014  cosf  12016  tanval2ap  12024  tanval3ap  12025  resin4p  12029  recos4p  12030  efival  12043  sinadd  12047  cosadd  12048  tanaddap  12050  pythagtriplem1  12588  pythagtriplem12  12598  pythagtriplem16  12602  pythagtriplem17  12603  pcbc  12674  mul4sqlem  12716  4sqlem14  12727  oddennn  12763  mulgdirlem  13489  gsumfzconst  13677  gsumfzfsumlemm  14349  addccncf  15072  limcimolemlt  15136  dvaddxxbr  15173  plyaddlem1  15219  ptolemy  15296  rpcxpadd  15377  binom4  15451  lgsquad2lem1  15558  2lgslem3d1  15577  qdencn  15966  iooref1o  15973  apdifflemr  15986