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

Axiom ax-icn 6977
Description: i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6937. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-icn i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 6889 . 2 class i
2 cc 6885 . 2 class
31, 2wcel 1393 1 wff i ∈ ℂ
Colors of variables: wff set class
This axiom is referenced by:  0cn  7017  mulid1  7022  cnegexlem2  7185  cnegex  7187  0cnALT  7199  negicn  7210  ine0  7389  ixi  7572  rimul  7574  rereim  7575  apreap  7576  cru  7591  apreim  7592  mulreim  7593  apadd1  7597  apneg  7600  recextlem1  7630  recexaplem2  7631  recexap  7632  crap0  7908  cju  7911  it0e0  8144  2mulicn  8145  iap0  8146  2muliap0  8147  cnref1o  8580  irec  9326  i2  9327  i3  9328  i4  9329  imval  9424  imre  9425  reim  9426  crre  9431  crim  9432  remim  9434  mulreap  9438  cjreb  9440  recj  9441  reneg  9442  readd  9443  remullem  9445  imcj  9449  imneg  9450  imadd  9451  cjadd  9458  cjneg  9464  imval2  9468  rei  9473  imi  9474  cji  9476  cjreim  9477  cjreim2  9478  cjap  9480  cnrecnv  9484  rennim  9574  absi  9631  absreimsq  9639  absreim  9640  absimle  9654  climcvg1nlem  9841
  Copyright terms: Public domain W3C validator