Theorem addcld 7505

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

Syntax hints:   -> wi 4   e. wcel 1438  (class class class)co 5652   CCcc 7346   + caddc 7351

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

This theorem is referenced by:  muladd11r  7636  negeu  7671  addsubass  7690  subsub2  7708  subsub4  7713  pnpcan  7719  pnncan  7721  addsub4  7723  pnpncand  7851  apreim  8078  addext  8085  divdirap  8162  recp1lt1  8358  cju  8419  cnref1o  9131  modsumfzodifsn  9799  ser3add  9931  expaddzap  9995  binom2  10061  binom3  10067  sqoddm1div8  10102  nn0opthlem1d  10124  reval  10279  imval  10280  crre  10287  remullem  10301  imval2  10324  cjreim2  10334  cnrecnv  10340  resqrexlemcalc1  10443  maxabslemab  10635  maxltsup  10647  max0addsup  10648  addcn2  10695  fsumadd  10796  isumadd  10821  binomlem  10873  efaddlem  10960  ef4p  10980  cosval  10990  cosf  10992  tanval2ap  11000  tanval3ap  11001  resin4p  11005  recos4p  11006  efival  11019  sinadd  11023  cosadd  11024  tanaddap  11026  oddennn  11479  qdencn  11870