Theorem 1cnd 7968

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7804  1c1 7807

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

This theorem is referenced by:  adddirp1d  7978  muladd11r  8107  recrecap  8660  rec11ap  8661  rec11rap  8662  rerecclap  8681  subrecap  8790  recp1lt1  8850  nn1m1nn  8931  add1p1  9162  sub1m1  9163  cnm2m1cnm3  9164  xp1d2m1eqxm1d2  9165  div4p1lem1div2  9166  peano2z  9283  zaddcllempos  9284  peano2zm  9285  zaddcllemneg  9286  nn0n0n1ge2  9317  zneo  9348  peano5uzti  9355  lincmb01cmp  9997  iccf1o  9998  nnsplit  10130  zpnn0elfzo1  10201  ubmelm1fzo  10219  fzoshftral  10231  exbtwnzlemstep  10241  rebtwn2zlemstep  10246  qbtwnrelemcalc  10249  flqaddz  10290  2tnp1ge0ge0  10294  ceiqm1l  10304  qnegmod  10362  addmodlteq  10391  uzsinds  10435  seq3shft2  10466  iseqf1olemab  10482  exp3val  10515  binom2sub1  10627  binom3  10630  zesq  10631  sqoddm1div8  10666  nn0opthlem1d  10691  bcm1k  10731  bcp1n  10732  bcp1m1  10736  bcpasc  10737  bcn2m1  10740  omgadd  10773  hashfz  10792  hashfzo  10793  hashfzp1  10795  zfz1isolemsplit  10809  zfz1isolem1  10811  resqrexlemover  11010  absexpzap  11080  reccn2ap  11312  hashiun  11477  hash2iun1dif1  11479  binomlem  11482  bcxmas  11488  arisum  11497  arisum2  11498  trireciplem  11499  geosergap  11505  pwm1geoserap1  11507  geolim  11510  geolim2  11511  georeclim  11512  geoisum1c  11519  cvgratnnlemnexp  11523  cvgratnnlemmn  11524  cvgratnnlemsumlt  11527  cvgratz  11531  mertenslemi1  11534  prodf1f  11542  prodfrecap  11545  ntrivcvgap  11547  prodrbdclem  11570  prodmodclem3  11574  prodmodclem2a  11575  zproddc  11578  fprodseq  11582  fprodntrivap  11583  prod1dc  11585  fprodmul  11590  prodsnf  11591  fprodsplitdc  11595  fprodm1  11597  fprodp1  11599  fprodcl  11606  fprodfac  11614  fprodrec  11628  fprodclf  11634  ef0lem  11659  efsub  11680  tanaddaplem  11737  tanaddap  11738  cos01bnd  11757  zeo3  11863  oddm1even  11870  oddp1even  11871  oexpneg  11872  ltoddhalfle  11888  halfleoddlt  11889  nn0ob  11903  flodddiv4  11929  bezoutlema  11990  bezoutlemb  11991  uzwodc  12028  qredeu  12087  prmdiv  12225  prmdiveq  12226  pc2dvds  12319  oddennn  12383  ennnfonelemp1  12397  cncrng  13268  dveflem  13969  dvef  13970  reeff1oleme  13975  sin0pilem1  13984  logdivlti  14084  rplogbval  14145  lgsvalmod  14202  lgsdir2  14216  lgsdir  14218  2sqlem8  14241  cvgcmp2nlemabs  14551  iooref1o  14553  trilpolemeq1  14559  trilpolemlt1  14560  apdifflemr  14566  iswomni0  14570  nconstwlpolemgt0  14582