Theorem 1cnd 8035

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7870  1c1 7873

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

This theorem is referenced by:  adddirp1d  8046  muladd11r  8175  recrecap  8728  rec11ap  8729  rec11rap  8730  rerecclap  8749  subrecap  8858  recp1lt1  8918  nn1m1nn  9000  add1p1  9232  sub1m1  9233  cnm2m1cnm3  9234  xp1d2m1eqxm1d2  9235  div4p1lem1div2  9236  peano2z  9353  zaddcllempos  9354  peano2zm  9355  zaddcllemneg  9356  nn0n0n1ge2  9387  zneo  9418  peano5uzti  9425  lincmb01cmp  10069  iccf1o  10070  nnsplit  10203  zpnn0elfzo1  10275  ubmelm1fzo  10293  fzoshftral  10305  exbtwnzlemstep  10316  rebtwn2zlemstep  10321  qbtwnrelemcalc  10324  flqaddz  10366  2tnp1ge0ge0  10370  ceiqm1l  10382  qnegmod  10440  addmodlteq  10469  uzsinds  10515  seq3shft2  10552  iseqf1olemab  10573  exp3val  10612  binom2sub1  10725  binom3  10728  zesq  10729  sqoddm1div8  10764  nn0opthlem1d  10791  bcm1k  10831  bcp1n  10832  bcp1m1  10836  bcpasc  10837  bcn2m1  10840  omgadd  10873  hashfz  10892  hashfzo  10893  hashfzp1  10895  zfz1isolemsplit  10909  zfz1isolem1  10911  resqrexlemover  11154  absexpzap  11224  reccn2ap  11456  hashiun  11621  hash2iun1dif1  11623  binomlem  11626  bcxmas  11632  arisum  11641  arisum2  11642  trireciplem  11643  geosergap  11649  pwm1geoserap1  11651  geolim  11654  geolim2  11655  georeclim  11656  geoisum1c  11663  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemsumlt  11671  cvgratz  11675  mertenslemi1  11678  prodf1f  11686  prodfrecap  11689  ntrivcvgap  11691  prodrbdclem  11714  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  fprodntrivap  11727  prod1dc  11729  fprodmul  11734  prodsnf  11735  fprodsplitdc  11739  fprodm1  11741  fprodp1  11743  fprodcl  11750  fprodfac  11758  fprodrec  11772  fprodclf  11778  ef0lem  11803  efsub  11824  tanaddaplem  11881  tanaddap  11882  cos01bnd  11901  zeo3  12009  oddm1even  12016  oddp1even  12017  oexpneg  12018  ltoddhalfle  12034  halfleoddlt  12035  nn0ob  12049  flodddiv4  12075  bezoutlema  12136  bezoutlemb  12137  uzwodc  12174  qredeu  12235  prmdiv  12373  prmdiveq  12374  pc2dvds  12468  4sqlem11  12539  4sqlem12  12540  oddennn  12549  ennnfonelemp1  12563  gsumfzconst  13411  cncrng  14057  hoverb  14802  dveflem  14872  dvef  14873  reeff1oleme  14907  sin0pilem1  14916  logdivlti  15016  rplogbval  15077  lgsvalmod  15135  lgsdir2  15149  lgsdir  15151  gausslemma2dlem1a  15174  gausslemma2dlem5  15182  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem1  15193  2sqlem8  15210  cvgcmp2nlemabs  15522  iooref1o  15524  trilpolemeq1  15530  trilpolemlt1  15531  apdifflemr  15537  iswomni0  15541  nconstwlpolemgt0  15554