Theorem 1cnd 7706

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

Step	Hyp	Ref	Expression
1		ax-1cn 7638	. 2 |- 1 e. CC
2	1	a1i 9	1 |- ( ph -> 1 e. CC )

Syntax hints:   -> wi 4   e. wcel 1463   CCcc 7545   1c1 7548

This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 7638

This theorem is referenced by:  adddirp1d  7716  muladd11r  7841  recrecap  8382  rec11ap  8383  rec11rap  8384  rerecclap  8403  recp1lt1  8567  nn1m1nn  8648  add1p1  8873  sub1m1  8874  cnm2m1cnm3  8875  xp1d2m1eqxm1d2  8876  div4p1lem1div2  8877  peano2z  8994  zaddcllempos  8995  peano2zm  8996  zaddcllemneg  8997  nn0n0n1ge2  9025  zneo  9056  peano5uzti  9063  lincmb01cmp  9679  iccf1o  9680  nnsplit  9807  zpnn0elfzo1  9878  ubmelm1fzo  9896  fzoshftral  9908  exbtwnzlemstep  9918  rebtwn2zlemstep  9923  qbtwnrelemcalc  9926  flqaddz  9963  2tnp1ge0ge0  9967  ceiqm1l  9977  qnegmod  10035  addmodlteq  10064  uzsinds  10108  seq3shft2  10139  iseqf1olemab  10155  exp3val  10188  binom2sub1  10299  binom3  10302  zesq  10303  sqoddm1div8  10337  nn0opthlem1d  10359  bcm1k  10399  bcp1n  10400  bcp1m1  10404  bcpasc  10405  bcn2m1  10408  omgadd  10441  hashfz  10460  hashfzo  10461  hashfzp1  10463  zfz1isolemsplit  10474  zfz1isolem1  10476  resqrexlemover  10674  absexpzap  10744  reccn2ap  10974  hashiun  11139  hash2iun1dif1  11141  binomlem  11144  bcxmas  11150  arisum  11159  arisum2  11160  trireciplem  11161  geosergap  11167  pwm1geoserap1  11169  geolim  11172  geolim2  11173  georeclim  11174  geoisum1c  11181  cvgratnnlemnexp  11185  cvgratnnlemmn  11186  cvgratnnlemsumlt  11189  cvgratz  11193  mertenslemi1  11196  ef0lem  11217  efsub  11238  tanaddaplem  11296  tanaddap  11297  cos01bnd  11316  zeo3  11413  oddm1even  11420  oddp1even  11421  oexpneg  11422  ltoddhalfle  11438  halfleoddlt  11439  nn0ob  11453  flodddiv4  11479  bezoutlema  11533  bezoutlemb  11534  qredeu  11624  oddennn  11750  ennnfonelemp1  11764  cvgcmp2nlemabs  12919  trilpolemeq1  12925  trilpolemlt1  12926