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

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

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 6739 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 6669   + caddc 6674
This theorem was proved from axioms:  ax-addcl 6739
This theorem is referenced by:  adddir  6776  0cn  6777  addcli  6789  addcld  6804  muladd11  6903  peano2cn  6905  add4  6929  cnegexlem3  6945  cnegex  6946  0cnALT  6958  negeu  6959  pncan  6974  2addsub  6982  addsubeq4  6983  nppcan2  6998  ppncan  7009  muladd  7137  mulsub  7154  recexap  7376  muleqadd  7391  conjmulap  7447  halfaddsubcl  7895  halfaddsub  7896  binom2  8975  binom3  8979  bernneq  8982  crre  9045  crim  9046  cjadd  9072  addcj  9079
  Copyright terms: Public domain W3C validator