Theorem addcld 7138

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 7098	. 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 1433  (class class class)co 5532   CCcc 6979   + caddc 6984

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

This theorem is referenced by:  muladd11r  7264  negeu  7299  addsubass  7318  subsub2  7336  subsub4  7341  pnpcan  7347  pnncan  7349  addsub4  7351  pnpncand  7479  apreim  7703  addext  7710  divdirap  7785  recp1lt1  7977  cju  8038  cnref1o  8733  modsumfzodifsn  9398  expaddzap  9520  binom2  9585  binom3  9590  sqoddm1div8  9625  nn0opthlem1d  9647  reval  9736  imval  9737  crre  9744  remullem  9758  imval2  9781  cjreim2  9791  cnrecnv  9797  resqrexlemcalc1  9900  maxabslemab  10092  maxltsup  10104  max0addsup  10105  addcn2  10149  qdencn  10785