Theorem 1cnd 7936

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 7867	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7772  1c1 7775

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

This theorem is referenced by:  adddirp1d  7946  muladd11r  8075  recrecap  8626  rec11ap  8627  rec11rap  8628  rerecclap  8647  subrecap  8756  recp1lt1  8815  nn1m1nn  8896  add1p1  9127  sub1m1  9128  cnm2m1cnm3  9129  xp1d2m1eqxm1d2  9130  div4p1lem1div2  9131  peano2z  9248  zaddcllempos  9249  peano2zm  9250  zaddcllemneg  9251  nn0n0n1ge2  9282  zneo  9313  peano5uzti  9320  lincmb01cmp  9960  iccf1o  9961  nnsplit  10093  zpnn0elfzo1  10164  ubmelm1fzo  10182  fzoshftral  10194  exbtwnzlemstep  10204  rebtwn2zlemstep  10209  qbtwnrelemcalc  10212  flqaddz  10253  2tnp1ge0ge0  10257  ceiqm1l  10267  qnegmod  10325  addmodlteq  10354  uzsinds  10398  seq3shft2  10429  iseqf1olemab  10445  exp3val  10478  binom2sub1  10590  binom3  10593  zesq  10594  sqoddm1div8  10629  nn0opthlem1d  10654  bcm1k  10694  bcp1n  10695  bcp1m1  10699  bcpasc  10700  bcn2m1  10703  omgadd  10737  hashfz  10756  hashfzo  10757  hashfzp1  10759  zfz1isolemsplit  10773  zfz1isolem1  10775  resqrexlemover  10974  absexpzap  11044  reccn2ap  11276  hashiun  11441  hash2iun1dif1  11443  binomlem  11446  bcxmas  11452  arisum  11461  arisum2  11462  trireciplem  11463  geosergap  11469  pwm1geoserap1  11471  geolim  11474  geolim2  11475  georeclim  11476  geoisum1c  11483  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemsumlt  11491  cvgratz  11495  mertenslemi1  11498  prodf1f  11506  prodfrecap  11509  ntrivcvgap  11511  prodrbdclem  11534  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodntrivap  11547  prod1dc  11549  fprodmul  11554  prodsnf  11555  fprodsplitdc  11559  fprodm1  11561  fprodp1  11563  fprodcl  11570  fprodfac  11578  fprodrec  11592  fprodclf  11598  ef0lem  11623  efsub  11644  tanaddaplem  11701  tanaddap  11702  cos01bnd  11721  zeo3  11827  oddm1even  11834  oddp1even  11835  oexpneg  11836  ltoddhalfle  11852  halfleoddlt  11853  nn0ob  11867  flodddiv4  11893  bezoutlema  11954  bezoutlemb  11955  uzwodc  11992  qredeu  12051  prmdiv  12189  prmdiveq  12190  pc2dvds  12283  oddennn  12347  ennnfonelemp1  12361  dveflem  13481  dvef  13482  reeff1oleme  13487  sin0pilem1  13496  logdivlti  13596  rplogbval  13657  lgsvalmod  13714  lgsdir2  13728  lgsdir  13730  2sqlem8  13753  cvgcmp2nlemabs  14064  iooref1o  14066  trilpolemeq1  14072  trilpolemlt1  14073  apdifflemr  14079  iswomni0  14083  nconstwlpolemgt0  14095