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

Theorem addcl 7149
Description: Alias for ax-addcl 7123, for naming consistency with addcli 7174. Use this theorem instead of ax-addcl 7123 or axaddcl 7083. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addcl ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 7123 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1434  (class class class)co 5537  cc 7030   + caddc 7035
This theorem was proved from axioms:  ax-addcl 7123
This theorem is referenced by:  adddir  7161  0cn  7162  addcli  7174  addcld  7189  muladd11  7297  peano2cn  7299  muladd11r  7320  add4  7325  cnegexlem3  7341  cnegex  7342  0cnALT  7354  negeu  7355  pncan  7370  2addsub  7378  addsubeq4  7379  nppcan2  7395  ppncan  7406  muladd  7544  mulsub  7561  recexap  7799  muleqadd  7814  conjmulap  7873  halfaddsubcl  8320  halfaddsub  8321  iserf  9538  iseradd  9548  isersub  9549  iser0  9557  serige0  9559  serile  9560  binom2  9671  binom3  9676  bernneq  9679  shftlem  9831  shftval2  9841  shftval5  9844  2shfti  9846  crre  9871  crim  9872  cjadd  9898  addcj  9905  sqabsadd  10068  absreimsq  10080  absreim  10081  abstri  10117  addcn2  10276  climadd  10291  clim2iser  10302  clim2iser2  10303  iisermulc2  10305  iserile  10307  climserile  10310  serif0  10316  isumrblem  10326  fisumcvg  10327  opoe  10428
  Copyright terms: Public domain W3C validator