Theorem 1cnd 8088

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

Syntax hints:   → wi 4   ∈ wcel 2176  ℂcc 7923  1c1 7926

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

This theorem is referenced by:  adddirp1d  8099  muladd11r  8228  muls1d  8490  recrecap  8782  rec11ap  8783  rec11rap  8784  rerecclap  8803  subrecap  8912  recp1lt1  8972  nn1m1nn  9054  add1p1  9287  sub1m1  9288  cnm2m1cnm3  9289  xp1d2m1eqxm1d2  9290  div4p1lem1div2  9291  peano2z  9408  zaddcllempos  9409  peano2zm  9410  zaddcllemneg  9411  nn0n0n1ge2  9443  zneo  9474  peano5uzti  9481  lincmb01cmp  10125  iccf1o  10126  nnsplit  10259  zpnn0elfzo1  10337  ubmelm1fzo  10355  fzoshftral  10367  exbtwnzlemstep  10390  rebtwn2zlemstep  10395  qbtwnrelemcalc  10398  flqaddz  10440  2tnp1ge0ge0  10444  ceiqm1l  10456  qnegmod  10514  addmodlteq  10543  uzsinds  10589  seq3shft2  10626  iseqf1olemab  10647  exp3val  10686  binom2sub1  10799  binom3  10802  zesq  10803  sqoddm1div8  10838  nn0opthlem1d  10865  bcm1k  10905  bcp1n  10906  bcp1m1  10910  bcpasc  10911  bcn2m1  10914  omgadd  10947  hashfz  10966  hashfzo  10967  hashfzp1  10969  zfz1isolemsplit  10983  zfz1isolem1  10985  lswccatn0lsw  11067  ccatws1lenp1bg  11089  lswccats1  11095  resqrexlemover  11321  absexpzap  11391  reccn2ap  11624  hashiun  11789  hash2iun1dif1  11791  binomlem  11794  bcxmas  11800  arisum  11809  arisum2  11810  trireciplem  11811  geosergap  11817  pwm1geoserap1  11819  geolim  11822  geolim2  11823  georeclim  11824  geoisum1c  11831  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  cvgratnnlemsumlt  11839  cvgratz  11843  mertenslemi1  11846  prodf1f  11854  prodfrecap  11857  ntrivcvgap  11859  prodrbdclem  11882  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodntrivap  11895  prod1dc  11897  fprodmul  11902  prodsnf  11903  fprodsplitdc  11907  fprodm1  11909  fprodp1  11911  fprodcl  11918  fprodfac  11926  fprodrec  11940  fprodclf  11946  ef0lem  11971  efsub  11992  tanaddaplem  12049  tanaddap  12050  cos01bnd  12069  zeo3  12179  oddm1even  12186  oddp1even  12187  oexpneg  12188  ltoddhalfle  12204  halfleoddlt  12205  nn0ob  12219  flodddiv4  12247  bitsp1o  12264  bezoutlema  12320  bezoutlemb  12321  uzwodc  12358  qredeu  12419  prmdiv  12557  prmdiveq  12558  pc2dvds  12653  4sqlem11  12724  4sqlem12  12725  oddennn  12763  ennnfonelemp1  12777  gsumfzconst  13677  cncrng  14331  expcn  15041  hoverb  15120  dveflem  15198  dvef  15199  dvply2g  15238  reeff1oleme  15244  sin0pilem1  15253  logdivlti  15353  rpcxpmul2  15385  rplogbval  15417  perfectlem2  15472  lgsvalmod  15496  lgsdir2  15510  lgsdir  15512  gausslemma2dlem1a  15535  gausslemma2dlem5  15543  lgseisenlem4  15550  lgsquadlem1  15554  m1lgs  15562  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgslem3d1  15577  2lgsoddprmlem1  15582  2sqlem8  15600  cvgcmp2nlemabs  15971  iooref1o  15973  trilpolemeq1  15979  trilpolemlt1  15980  apdifflemr  15986  iswomni0  15990  nconstwlpolemgt0  16003