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

Theorem addcl 6804
Description: Alias for ax-addcl 6779, for naming consistency with addcli 6829. Use this theorem instead of ax-addcl 6779 or axaddcl 6750. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addcl ((A B ℂ) → (A + B) ℂ)

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 6779 1 ((A B ℂ) → (A + B) ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1390  (class class class)co 5455  cc 6709   + caddc 6714
This theorem was proved from axioms:  ax-addcl 6779
This theorem is referenced by:  adddir  6816  0cn  6817  addcli  6829  addcld  6844  muladd11  6943  peano2cn  6945  add4  6969  cnegexlem3  6985  cnegex  6986  0cnALT  6998  negeu  6999  pncan  7014  2addsub  7022  addsubeq4  7023  nppcan2  7038  ppncan  7049  muladd  7177  mulsub  7194  recexap  7416  muleqadd  7431  conjmulap  7487  halfaddsubcl  7935  halfaddsub  7936  binom2  9015  binom3  9019  bernneq  9022  crre  9085  crim  9086  cjadd  9112  addcj  9119
  Copyright terms: Public domain W3C validator