Theorem 1cnd 8037

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7872  1c1 7875

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

This theorem is referenced by:  adddirp1d  8048  muladd11r  8177  recrecap  8730  rec11ap  8731  rec11rap  8732  rerecclap  8751  subrecap  8860  recp1lt1  8920  nn1m1nn  9002  add1p1  9235  sub1m1  9236  cnm2m1cnm3  9237  xp1d2m1eqxm1d2  9238  div4p1lem1div2  9239  peano2z  9356  zaddcllempos  9357  peano2zm  9358  zaddcllemneg  9359  nn0n0n1ge2  9390  zneo  9421  peano5uzti  9428  lincmb01cmp  10072  iccf1o  10073  nnsplit  10206  zpnn0elfzo1  10278  ubmelm1fzo  10296  fzoshftral  10308  exbtwnzlemstep  10319  rebtwn2zlemstep  10324  qbtwnrelemcalc  10327  flqaddz  10369  2tnp1ge0ge0  10373  ceiqm1l  10385  qnegmod  10443  addmodlteq  10472  uzsinds  10518  seq3shft2  10555  iseqf1olemab  10576  exp3val  10615  binom2sub1  10728  binom3  10731  zesq  10732  sqoddm1div8  10767  nn0opthlem1d  10794  bcm1k  10834  bcp1n  10835  bcp1m1  10839  bcpasc  10840  bcn2m1  10843  omgadd  10876  hashfz  10895  hashfzo  10896  hashfzp1  10898  zfz1isolemsplit  10912  zfz1isolem1  10914  resqrexlemover  11157  absexpzap  11227  reccn2ap  11459  hashiun  11624  hash2iun1dif1  11626  binomlem  11629  bcxmas  11635  arisum  11644  arisum2  11645  trireciplem  11646  geosergap  11652  pwm1geoserap1  11654  geolim  11657  geolim2  11658  georeclim  11659  geoisum1c  11666  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratnnlemsumlt  11674  cvgratz  11678  mertenslemi1  11681  prodf1f  11689  prodfrecap  11692  ntrivcvgap  11694  prodrbdclem  11717  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodntrivap  11730  prod1dc  11732  fprodmul  11737  prodsnf  11738  fprodsplitdc  11742  fprodm1  11744  fprodp1  11746  fprodcl  11753  fprodfac  11761  fprodrec  11775  fprodclf  11781  ef0lem  11806  efsub  11827  tanaddaplem  11884  tanaddap  11885  cos01bnd  11904  zeo3  12012  oddm1even  12019  oddp1even  12020  oexpneg  12021  ltoddhalfle  12037  halfleoddlt  12038  nn0ob  12052  flodddiv4  12078  bezoutlema  12139  bezoutlemb  12140  uzwodc  12177  qredeu  12238  prmdiv  12376  prmdiveq  12377  pc2dvds  12471  4sqlem11  12542  4sqlem12  12543  oddennn  12552  ennnfonelemp1  12566  gsumfzconst  13414  cncrng  14068  expcn  14748  hoverb  14827  dveflem  14905  dvef  14906  reeff1oleme  14948  sin0pilem1  14957  logdivlti  15057  rplogbval  15118  lgsvalmod  15176  lgsdir2  15190  lgsdir  15192  gausslemma2dlem1a  15215  gausslemma2dlem5  15223  lgseisenlem4  15230  lgsquadlem1  15234  m1lgs  15242  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgslem3d1  15257  2lgsoddprmlem1  15262  2sqlem8  15280  cvgcmp2nlemabs  15592  iooref1o  15594  trilpolemeq1  15600  trilpolemlt1  15601  apdifflemr  15607  iswomni0  15611  nconstwlpolemgt0  15624