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

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

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 6978 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wcel 1393  (class class class)co 5512  cc 6885   + caddc 6890
This theorem was proved from axioms:  ax-addcl 6978
This theorem is referenced by:  adddir  7016  0cn  7017  addcli  7029  addcld  7044  muladd11  7144  peano2cn  7146  add4  7170  cnegexlem3  7186  cnegex  7187  0cnALT  7199  negeu  7200  pncan  7215  2addsub  7223  addsubeq4  7224  nppcan2  7240  ppncan  7251  muladd  7379  mulsub  7396  recexap  7632  muleqadd  7647  conjmulap  7703  halfaddsubcl  8156  halfaddsub  8157  iserf  9207  iseradd  9217  isersub  9218  iser0  9224  iser0f  9225  serige0  9226  serile  9227  binom2  9336  binom3  9340  bernneq  9343  shftlem  9391  shftval2  9401  shftval5  9404  2shfti  9406  crre  9431  crim  9432  cjadd  9458  addcj  9465  sqabsadd  9627  absreimsq  9639  absreim  9640  abstri  9674  addcn2  9805  climadd  9820  clim2iser  9831  clim2iser2  9832  iisermulc2  9834  iserile  9836  climserile  9839  serif0  9845
  Copyright terms: Public domain W3C validator