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

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

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 6949 . 2 class i
2 cc 6945 . 2 class
31, 2wcel 1409 1 wff i ∈ ℂ
Colors of variables: wff set class
This axiom is referenced by:  0cn  7077  mulid1  7082  cnegexlem2  7250  cnegex  7252  0cnALT  7264  negicn  7275  ine0  7463  ixi  7648  rimul  7650  rereim  7651  apreap  7652  cru  7667  apreim  7668  mulreim  7669  apadd1  7673  apneg  7676  recextlem1  7706  recexaplem2  7707  recexap  7708  crap0  7986  cju  7989  it0e0  8203  2mulicn  8204  iap0  8205  2muliap0  8206  cnref1o  8680  irec  9518  i2  9519  i3  9520  i4  9521  iexpcyc  9523  imval  9678  imre  9679  reim  9680  crre  9685  crim  9686  remim  9688  mulreap  9692  cjreb  9694  recj  9695  reneg  9696  readd  9697  remullem  9699  imcj  9703  imneg  9704  imadd  9705  cjadd  9712  cjneg  9718  imval2  9722  rei  9727  imi  9728  cji  9730  cjreim  9731  cjreim2  9732  cjap  9734  cnrecnv  9738  rennim  9829  absi  9886  absreimsq  9894  absreim  9895  absimle  9911  climcvg1nlem  10099  qdencn  10511
  Copyright terms: Public domain W3C validator