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

Theorem addcld 8002
Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
addcld (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcld
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addcl 7961 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3syl2anc 411 1 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2160  (class class class)co 5892  cc 7834   + caddc 7839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addcl 7932
This theorem is referenced by:  muladd11r  8138  negeu  8173  addsubass  8192  subsub2  8210  subsub4  8215  pnpcan  8221  pnncan  8223  addsub4  8225  pnpncand  8357  apreim  8585  addext  8592  aprcl  8628  aptap  8632  divdirap  8679  recp1lt1  8881  cju  8943  cnref1o  9675  modsumfzodifsn  10422  expaddzap  10590  binom2  10658  binom3  10664  sqoddm1div8  10700  mulsubdivbinom2ap  10718  nn0opthlem1d  10727  reval  10885  imval  10886  crre  10893  remullem  10907  imval2  10930  cjreim2  10940  cnrecnv  10946  resqrexlemcalc1  11050  maxabslemab  11242  maxltsup  11254  max0addsup  11255  minabs  11271  bdtrilem  11274  bdtri  11275  addcn2  11345  fsumadd  11441  isumadd  11466  binomlem  11518  efaddlem  11709  ef4p  11729  cosval  11738  cosf  11740  tanval2ap  11748  tanval3ap  11749  resin4p  11753  recos4p  11754  efival  11767  sinadd  11771  cosadd  11772  tanaddap  11774  pythagtriplem1  12292  pythagtriplem12  12302  pythagtriplem16  12306  pythagtriplem17  12307  pcbc  12378  mul4sqlem  12420  4sqlem14  12431  oddennn  12438  mulgdirlem  13086  addccncf  14523  limcimolemlt  14570  dvaddxxbr  14602  ptolemy  14682  rpcxpadd  14763  binom4  14834  qdencn  15213  iooref1o  15220  apdifflemr  15233
  Copyright terms: Public domain W3C validator