Theorem 1cnd 8306

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8141  1c1 8144

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

This theorem is referenced by:  adddirp1d  8316  muladd11r  8445  muls1d  8708  recrecap  9000  rec11ap  9001  rec11rap  9002  rerecclap  9021  subrecap  9130  recp1lt1  9190  nn1m1nn  9272  add1p1  9505  sub1m1  9506  cnm2m1cnm3  9507  xp1d2m1eqxm1d2  9508  div4p1lem1div2  9509  peano2z  9630  zaddcllempos  9631  peano2zm  9632  zaddcllemneg  9633  nn0n0n1ge2  9665  zneo  9697  peano5uzti  9704  ltesubnnd  10120  lincmb01cmp  10355  lincmble  10356  iccf1o  10357  fzsplit3  10407  nnsplit  10493  zpnn0elfzo1  10575  ubmelm1fzo  10593  fzosplitpr  10601  fzoshftral  10606  exbtwnzlemstep  10631  rebtwn2zlemstep  10636  qbtwnrelemcalc  10639  flqaddz  10681  2tnp1ge0ge0  10685  ceiqm1l  10697  qnegmod  10755  addmodlteq  10784  uzsinds  10830  seq3shft2  10867  iseqf1olemab  10888  exp3val  10927  binom2sub1  11040  binom3  11043  zesq  11045  sqoddm1div8  11080  nn0opthlem1d  11107  bcm1k  11147  bcp1n  11148  bcp1m1  11152  bcpasc  11153  bcm1n  11156  bcn2m1  11157  omgadd  11191  hashfz  11211  hashfzo  11212  hashfzp1  11214  zfz1isolemsplit  11235  zfz1isolem1  11237  lswccatn0lsw  11324  ccatws1lenp1bg  11348  lswccats1  11356  resqrexlemover  11720  absexpzap  11790  reccn2ap  12023  hashiun  12189  hash2iun1dif1  12191  binomlem  12194  bcxmas  12200  arisum  12209  arisum2  12210  trireciplem  12211  geosergap  12217  pwm1geoserap1  12219  geolim  12222  geolim2  12223  georeclim  12224  geoisum1c  12231  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemsumlt  12239  cvgratz  12243  mertenslemi1  12246  prodf1f  12254  prodfrecap  12257  ntrivcvgap  12259  prodrbdclem  12282  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodntrivap  12295  prod1dc  12297  fprodmul  12302  prodsnf  12303  fprodsplitdc  12307  fprodm1  12309  fprodp1  12311  fprodcl  12318  fprodfac  12326  fprodrec  12340  fprodclf  12346  ef0lem  12371  efsub  12392  tanaddaplem  12449  tanaddap  12450  cos01bnd  12469  zeo3  12579  oddm1even  12586  oddp1even  12587  oexpneg  12588  ltoddhalfle  12604  halfleoddlt  12605  nn0ob  12619  flodddiv4  12647  bitsp1o  12664  bezoutlema  12720  bezoutlemb  12721  uzwodc  12758  qredeu  12819  prmdiv  12957  prmdiveq  12958  pc2dvds  13053  4sqlem11  13124  4sqlem12  13125  ballotfilemfp1  13175  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsgt1  13198  ballotfilemsdom  13199  ballotfilemsel1i  13200  ballotfilemsi  13202  ballotfilemsima  13203  ballotfilem1ri  13222  oddennn  13227  ennnfonelemp1  13241  gsumfzconst  14094  gsumsplit0  14099  gsumshift  14105  gsumgfsum  14106  cncrng  14843  expcn  15560  hoverb  15639  dveflem  15717  dvef  15718  dvply2g  15757  reeff1oleme  15763  sin0pilem1  15772  logdivlti  15872  rpcxpmul2  15904  rplogbval  15936  perfectlem2  15994  lgsvalmod  16018  lgsdir2  16032  lgsdir  16034  gausslemma2dlem1a  16057  gausslemma2dlem5  16065  lgseisenlem4  16072  lgsquadlem1  16076  m1lgs  16084  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgslem3d1  16099  2lgsoddprmlem1  16104  2sqlem8  16122  wlklenvclwlk  16494  clwwlkccatlem  16521  clwwlkext2edg  16543  clwwlknonex2lem1  16558  clwwlknonex2lem2  16559  cvgcmp2nlemabs  16942  iooref1o  16944  trilpolemeq1  16950  trilpolemlt1  16951  apdifflemr  16957  qdiff  16959  iswomni0  16962  nconstwlpolemgt0  16976