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

Theorem addcld 7792
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 7752 . 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 1480  (class class class)co 5774   CCcc 7625    + caddc 7630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-addcl 7723
This theorem is referenced by:  muladd11r  7925  negeu  7960  addsubass  7979  subsub2  7997  subsub4  8002  pnpcan  8008  pnncan  8010  addsub4  8012  pnpncand  8144  apreim  8372  addext  8379  aprcl  8415  divdirap  8464  recp1lt1  8664  cju  8726  cnref1o  9447  modsumfzodifsn  10176  expaddzap  10344  binom2  10410  binom3  10416  sqoddm1div8  10451  nn0opthlem1d  10473  reval  10628  imval  10629  crre  10636  remullem  10650  imval2  10673  cjreim2  10683  cnrecnv  10689  resqrexlemcalc1  10793  maxabslemab  10985  maxltsup  10997  max0addsup  10998  minabs  11014  bdtrilem  11017  bdtri  11018  addcn2  11086  fsumadd  11182  isumadd  11207  binomlem  11259  efaddlem  11387  ef4p  11407  cosval  11417  cosf  11419  tanval2ap  11427  tanval3ap  11428  resin4p  11432  recos4p  11433  efival  11446  sinadd  11450  cosadd  11451  tanaddap  11453  oddennn  11912  addccncf  12765  limcimolemlt  12812  dvaddxxbr  12844  ptolemy  12915  qdencn  13236
  Copyright terms: Public domain W3C validator