Theorem 1cnd 8061

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7896  1c1 7899

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

This theorem is referenced by:  adddirp1d  8072  muladd11r  8201  muls1d  8463  recrecap  8755  rec11ap  8756  rec11rap  8757  rerecclap  8776  subrecap  8885  recp1lt1  8945  nn1m1nn  9027  add1p1  9260  sub1m1  9261  cnm2m1cnm3  9262  xp1d2m1eqxm1d2  9263  div4p1lem1div2  9264  peano2z  9381  zaddcllempos  9382  peano2zm  9383  zaddcllemneg  9384  nn0n0n1ge2  9415  zneo  9446  peano5uzti  9453  lincmb01cmp  10097  iccf1o  10098  nnsplit  10231  zpnn0elfzo1  10303  ubmelm1fzo  10321  fzoshftral  10333  exbtwnzlemstep  10356  rebtwn2zlemstep  10361  qbtwnrelemcalc  10364  flqaddz  10406  2tnp1ge0ge0  10410  ceiqm1l  10422  qnegmod  10480  addmodlteq  10509  uzsinds  10555  seq3shft2  10592  iseqf1olemab  10613  exp3val  10652  binom2sub1  10765  binom3  10768  zesq  10769  sqoddm1div8  10804  nn0opthlem1d  10831  bcm1k  10871  bcp1n  10872  bcp1m1  10876  bcpasc  10877  bcn2m1  10880  omgadd  10913  hashfz  10932  hashfzo  10933  hashfzp1  10935  zfz1isolemsplit  10949  zfz1isolem1  10951  resqrexlemover  11194  absexpzap  11264  reccn2ap  11497  hashiun  11662  hash2iun1dif1  11664  binomlem  11667  bcxmas  11673  arisum  11682  arisum2  11683  trireciplem  11684  geosergap  11690  pwm1geoserap1  11692  geolim  11695  geolim2  11696  georeclim  11697  geoisum1c  11704  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemsumlt  11712  cvgratz  11716  mertenslemi1  11719  prodf1f  11727  prodfrecap  11730  ntrivcvgap  11732  prodrbdclem  11755  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  fprodntrivap  11768  prod1dc  11770  fprodmul  11775  prodsnf  11776  fprodsplitdc  11780  fprodm1  11782  fprodp1  11784  fprodcl  11791  fprodfac  11799  fprodrec  11813  fprodclf  11819  ef0lem  11844  efsub  11865  tanaddaplem  11922  tanaddap  11923  cos01bnd  11942  zeo3  12052  oddm1even  12059  oddp1even  12060  oexpneg  12061  ltoddhalfle  12077  halfleoddlt  12078  nn0ob  12092  flodddiv4  12120  bitsp1o  12137  bezoutlema  12193  bezoutlemb  12194  uzwodc  12231  qredeu  12292  prmdiv  12430  prmdiveq  12431  pc2dvds  12526  4sqlem11  12597  4sqlem12  12598  oddennn  12636  ennnfonelemp1  12650  gsumfzconst  13549  cncrng  14203  expcn  14913  hoverb  14992  dveflem  15070  dvef  15071  dvply2g  15110  reeff1oleme  15116  sin0pilem1  15125  logdivlti  15225  rpcxpmul2  15257  rplogbval  15289  perfectlem2  15344  lgsvalmod  15368  lgsdir2  15382  lgsdir  15384  gausslemma2dlem1a  15407  gausslemma2dlem5  15415  lgseisenlem4  15422  lgsquadlem1  15426  m1lgs  15434  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgslem3d1  15449  2lgsoddprmlem1  15454  2sqlem8  15472  cvgcmp2nlemabs  15789  iooref1o  15791  trilpolemeq1  15797  trilpolemlt1  15798  apdifflemr  15804  iswomni0  15808  nconstwlpolemgt0  15821