Theorem 1cnd 8123

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

Syntax hints:   → wi 4   ∈ wcel 2178  ℂcc 7958  1c1 7961

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

This theorem is referenced by:  adddirp1d  8134  muladd11r  8263  muls1d  8525  recrecap  8817  rec11ap  8818  rec11rap  8819  rerecclap  8838  subrecap  8947  recp1lt1  9007  nn1m1nn  9089  add1p1  9322  sub1m1  9323  cnm2m1cnm3  9324  xp1d2m1eqxm1d2  9325  div4p1lem1div2  9326  peano2z  9443  zaddcllempos  9444  peano2zm  9445  zaddcllemneg  9446  nn0n0n1ge2  9478  zneo  9509  peano5uzti  9516  lincmb01cmp  10160  iccf1o  10161  nnsplit  10294  zpnn0elfzo1  10374  ubmelm1fzo  10392  fzoshftral  10404  exbtwnzlemstep  10427  rebtwn2zlemstep  10432  qbtwnrelemcalc  10435  flqaddz  10477  2tnp1ge0ge0  10481  ceiqm1l  10493  qnegmod  10551  addmodlteq  10580  uzsinds  10626  seq3shft2  10663  iseqf1olemab  10684  exp3val  10723  binom2sub1  10836  binom3  10839  zesq  10840  sqoddm1div8  10875  nn0opthlem1d  10902  bcm1k  10942  bcp1n  10943  bcp1m1  10947  bcpasc  10948  bcn2m1  10951  omgadd  10984  hashfz  11003  hashfzo  11004  hashfzp1  11006  zfz1isolemsplit  11020  zfz1isolem1  11022  lswccatn0lsw  11105  ccatws1lenp1bg  11127  lswccats1  11133  resqrexlemover  11436  absexpzap  11506  reccn2ap  11739  hashiun  11904  hash2iun1dif1  11906  binomlem  11909  bcxmas  11915  arisum  11924  arisum2  11925  trireciplem  11926  geosergap  11932  pwm1geoserap1  11934  geolim  11937  geolim2  11938  georeclim  11939  geoisum1c  11946  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratnnlemsumlt  11954  cvgratz  11958  mertenslemi1  11961  prodf1f  11969  prodfrecap  11972  ntrivcvgap  11974  prodrbdclem  11997  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodntrivap  12010  prod1dc  12012  fprodmul  12017  prodsnf  12018  fprodsplitdc  12022  fprodm1  12024  fprodp1  12026  fprodcl  12033  fprodfac  12041  fprodrec  12055  fprodclf  12061  ef0lem  12086  efsub  12107  tanaddaplem  12164  tanaddap  12165  cos01bnd  12184  zeo3  12294  oddm1even  12301  oddp1even  12302  oexpneg  12303  ltoddhalfle  12319  halfleoddlt  12320  nn0ob  12334  flodddiv4  12362  bitsp1o  12379  bezoutlema  12435  bezoutlemb  12436  uzwodc  12473  qredeu  12534  prmdiv  12672  prmdiveq  12673  pc2dvds  12768  4sqlem11  12839  4sqlem12  12840  oddennn  12878  ennnfonelemp1  12892  gsumfzconst  13792  cncrng  14446  expcn  15156  hoverb  15235  dveflem  15313  dvef  15314  dvply2g  15353  reeff1oleme  15359  sin0pilem1  15368  logdivlti  15468  rpcxpmul2  15500  rplogbval  15532  perfectlem2  15587  lgsvalmod  15611  lgsdir2  15625  lgsdir  15627  gausslemma2dlem1a  15650  gausslemma2dlem5  15658  lgseisenlem4  15665  lgsquadlem1  15669  m1lgs  15677  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgslem3d1  15692  2lgsoddprmlem1  15697  2sqlem8  15715  cvgcmp2nlemabs  16173  iooref1o  16175  trilpolemeq1  16181  trilpolemlt1  16182  apdifflemr  16188  iswomni0  16192  nconstwlpolemgt0  16205