Theorem 1cnd 7565

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

Syntax hints:   → wi 4   ∈ wcel 1439  ℂcc 7409  1c1 7412

This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 7499

This theorem is referenced by:  adddirp1d  7575  muladd11r  7699  recrecap  8237  rec11ap  8238  rec11rap  8239  rerecclap  8258  recp1lt1  8421  nn1m1nn  8501  add1p1  8726  sub1m1  8727  cnm2m1cnm3  8728  xp1d2m1eqxm1d2  8729  div4p1lem1div2  8730  peano2z  8847  zaddcllempos  8848  peano2zm  8849  zaddcllemneg  8850  nn0n0n1ge2  8878  zneo  8908  peano5uzti  8915  lincmb01cmp  9481  iccf1o  9482  nnsplit  9609  zpnn0elfzo1  9680  ubmelm1fzo  9698  fzoshftral  9710  exbtwnzlemstep  9720  rebtwn2zlemstep  9725  qbtwnrelemcalc  9728  flqaddz  9765  2tnp1ge0ge0  9769  ceiqm1l  9779  qnegmod  9837  addmodlteq  9866  uzsinds  9909  iseqf1olemab  9979  exp3val  10018  binom2sub1  10129  binom3  10132  zesq  10133  sqoddm1div8  10167  nn0opthlem1d  10189  bcm1k  10229  bcp1n  10230  bcp1m1  10234  bcpasc  10235  bcn2m1  10238  omgadd  10271  hashfz  10290  hashfzo  10291  hashfzp1  10293  zfz1isolemsplit  10304  zfz1isolem1  10306  resqrexlemover  10504  absexpzap  10574  hashiun  10933  hash2iun1dif1  10935  binomlem  10938  bcxmas  10944  arisum  10953  arisum2  10954  trireciplem  10955  geosergap  10961  pwm1geoserap1  10963  geolim  10966  geolim2  10967  georeclim  10968  geoisum1c  10975  cvgratnnlemnexp  10979  cvgratnnlemmn  10980  cvgratnnlemsumlt  10983  cvgratz  10987  mertenslemi1  10990  ef0lem  11011  efsub  11032  tanaddaplem  11090  tanaddap  11091  cos01bnd  11110  zeo3  11207  oddm1even  11214  oddp1even  11215  oexpneg  11216  ltoddhalfle  11232  halfleoddlt  11233  nn0ob  11247  flodddiv4  11273  bezoutlema  11327  bezoutlemb  11328  qredeu  11418  oddennn  11544