ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  1cnd Unicode version

Theorem 1cnd 7186
Description: 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1cnd  |-  ( ph  ->  1  e.  CC )

Proof of Theorem 1cnd
StepHypRef Expression
1 ax-1cn 7120 . 2  |-  1  e.  CC
21a1i 9 1  |-  ( ph  ->  1  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   CCcc 7030   1c1 7033
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 7120
This theorem is referenced by:  adddirp1d  7196  muladd11r  7320  recrecap  7853  rec11ap  7854  rec11rap  7855  rerecclap  7874  recp1lt1  8033  nn1m1nn  8113  add1p1  8336  sub1m1  8337  cnm2m1cnm3  8338  xp1d2m1eqxm1d2  8339  div4p1lem1div2  8340  peano2z  8457  zaddcllempos  8458  peano2zm  8459  zaddcllemneg  8460  nn0n0n1ge2  8488  zneo  8518  peano5uzti  8525  lincmb01cmp  9090  iccf1o  9091  zpnn0elfzo1  9283  ubmelm1fzo  9301  fzoshftral  9313  exbtwnzlemstep  9323  rebtwn2zlemstep  9328  qbtwnrelemcalc  9331  flqaddz  9368  2tnp1ge0ge0  9372  ceiqm1l  9382  qnegmod  9440  addmodlteq  9469  uzsinds  9507  binom3  9676  zesq  9677  sqoddm1div8  9711  nn0opthlem1d  9733  bcm1k  9773  bcp1n  9774  bcp1m1  9778  bcpasc  9779  bcn2m1  9782  omgadd  9815  resqrexlemover  10023  absexpzap  10093  zeo3  10401  oddm1even  10408  oddp1even  10409  oexpneg  10410  ltoddhalfle  10426  halfleoddlt  10427  nn0ob  10441  flodddiv4  10467  bezoutlema  10521  bezoutlemb  10522  qredeu  10612  oddennn  10692
  Copyright terms: Public domain W3C validator