Theorem 1cnd 7915

Description: 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1cnd	⊢ (𝜑 → 1 ∈ ℂ)

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 7846	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 7751  1c1 7754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 7846

This theorem is referenced by:  adddirp1d  7925  muladd11r  8054  recrecap  8605  rec11ap  8606  rec11rap  8607  rerecclap  8626  subrecap  8735  recp1lt1  8794  nn1m1nn  8875  add1p1  9106  sub1m1  9107  cnm2m1cnm3  9108  xp1d2m1eqxm1d2  9109  div4p1lem1div2  9110  peano2z  9227  zaddcllempos  9228  peano2zm  9229  zaddcllemneg  9230  nn0n0n1ge2  9261  zneo  9292  peano5uzti  9299  lincmb01cmp  9939  iccf1o  9940  nnsplit  10072  zpnn0elfzo1  10143  ubmelm1fzo  10161  fzoshftral  10173  exbtwnzlemstep  10183  rebtwn2zlemstep  10188  qbtwnrelemcalc  10191  flqaddz  10232  2tnp1ge0ge0  10236  ceiqm1l  10246  qnegmod  10304  addmodlteq  10333  uzsinds  10377  seq3shft2  10408  iseqf1olemab  10424  exp3val  10457  binom2sub1  10569  binom3  10572  zesq  10573  sqoddm1div8  10608  nn0opthlem1d  10633  bcm1k  10673  bcp1n  10674  bcp1m1  10678  bcpasc  10679  bcn2m1  10682  omgadd  10715  hashfz  10734  hashfzo  10735  hashfzp1  10737  zfz1isolemsplit  10751  zfz1isolem1  10753  resqrexlemover  10952  absexpzap  11022  reccn2ap  11254  hashiun  11419  hash2iun1dif1  11421  binomlem  11424  bcxmas  11430  arisum  11439  arisum2  11440  trireciplem  11441  geosergap  11447  pwm1geoserap1  11449  geolim  11452  geolim2  11453  georeclim  11454  geoisum1c  11461  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemsumlt  11469  cvgratz  11473  mertenslemi1  11476  prodf1f  11484  prodfrecap  11487  ntrivcvgap  11489  prodrbdclem  11512  prodmodclem3  11516  prodmodclem2a  11517  zproddc  11520  fprodseq  11524  fprodntrivap  11525  prod1dc  11527  fprodmul  11532  prodsnf  11533  fprodsplitdc  11537  fprodm1  11539  fprodp1  11541  fprodcl  11548  fprodfac  11556  fprodrec  11570  fprodclf  11576  ef0lem  11601  efsub  11622  tanaddaplem  11679  tanaddap  11680  cos01bnd  11699  zeo3  11805  oddm1even  11812  oddp1even  11813  oexpneg  11814  ltoddhalfle  11830  halfleoddlt  11831  nn0ob  11845  flodddiv4  11871  bezoutlema  11932  bezoutlemb  11933  uzwodc  11970  qredeu  12029  prmdiv  12167  prmdiveq  12168  pc2dvds  12261  oddennn  12325  ennnfonelemp1  12339  dveflem  13337  dvef  13338  reeff1oleme  13343  sin0pilem1  13352  logdivlti  13452  rplogbval  13513  lgsvalmod  13570  lgsdir2  13584  lgsdir  13586  2sqlem8  13609  cvgcmp2nlemabs  13921  iooref1o  13923  trilpolemeq1  13929  trilpolemlt1  13930  apdifflemr  13936  iswomni0  13940  nconstwlpolemgt0  13952