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

Theorem addcld 7797
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 7757 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3syl2anc 408 1 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1480  (class class class)co 5774  cc 7630   + caddc 7635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-addcl 7728
This theorem is referenced by:  muladd11r  7930  negeu  7965  addsubass  7984  subsub2  8002  subsub4  8007  pnpcan  8013  pnncan  8015  addsub4  8017  pnpncand  8149  apreim  8377  addext  8384  aprcl  8420  divdirap  8469  recp1lt1  8669  cju  8731  cnref1o  9452  modsumfzodifsn  10181  expaddzap  10349  binom2  10415  binom3  10421  sqoddm1div8  10456  nn0opthlem1d  10478  reval  10633  imval  10634  crre  10641  remullem  10655  imval2  10678  cjreim2  10688  cnrecnv  10694  resqrexlemcalc1  10798  maxabslemab  10990  maxltsup  11002  max0addsup  11003  minabs  11019  bdtrilem  11022  bdtri  11023  addcn2  11091  fsumadd  11187  isumadd  11212  binomlem  11264  efaddlem  11392  ef4p  11412  cosval  11421  cosf  11423  tanval2ap  11431  tanval3ap  11432  resin4p  11436  recos4p  11437  efival  11450  sinadd  11454  cosadd  11455  tanaddap  11457  oddennn  11916  addccncf  12769  limcimolemlt  12816  dvaddxxbr  12848  ptolemy  12927  rpcxpadd  13005  qdencn  13329  apdifflemr  13347
  Copyright terms: Public domain W3C validator