ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addcld Unicode version

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
StepHypRef 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 )
41, 2, 3syl2anc 403 1  |-  ( ph  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator