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

Theorem addcld 7753
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 7713 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3syl2anc 408 1  |-  ( ph  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1465  (class class class)co 5742   CCcc 7586    + caddc 7591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-addcl 7684
This theorem is referenced by:  muladd11r  7886  negeu  7921  addsubass  7940  subsub2  7958  subsub4  7963  pnpcan  7969  pnncan  7971  addsub4  7973  pnpncand  8105  apreim  8333  addext  8340  aprcl  8376  divdirap  8425  recp1lt1  8625  cju  8687  cnref1o  9408  modsumfzodifsn  10137  expaddzap  10305  binom2  10371  binom3  10377  sqoddm1div8  10412  nn0opthlem1d  10434  reval  10589  imval  10590  crre  10597  remullem  10611  imval2  10634  cjreim2  10644  cnrecnv  10650  resqrexlemcalc1  10754  maxabslemab  10946  maxltsup  10958  max0addsup  10959  minabs  10975  bdtrilem  10978  bdtri  10979  addcn2  11047  fsumadd  11143  isumadd  11168  binomlem  11220  efaddlem  11307  ef4p  11327  cosval  11337  cosf  11339  tanval2ap  11347  tanval3ap  11348  resin4p  11352  recos4p  11353  efival  11366  sinadd  11370  cosadd  11371  tanaddap  11373  oddennn  11832  addccncf  12682  limcimolemlt  12729  dvaddxxbr  12761  ptolemy  12832  qdencn  13149
  Copyright terms: Public domain W3C validator