Theorem 1cnd 7806

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

Syntax hints:   → wi 4   ∈ wcel 1481  ℂcc 7642  1c1 7645

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

This theorem is referenced by:  adddirp1d  7816  muladd11r  7942  recrecap  8493  rec11ap  8494  rec11rap  8495  rerecclap  8514  subrecap  8622  recp1lt1  8681  nn1m1nn  8762  add1p1  8993  sub1m1  8994  cnm2m1cnm3  8995  xp1d2m1eqxm1d2  8996  div4p1lem1div2  8997  peano2z  9114  zaddcllempos  9115  peano2zm  9116  zaddcllemneg  9117  nn0n0n1ge2  9145  zneo  9176  peano5uzti  9183  lincmb01cmp  9816  iccf1o  9817  nnsplit  9945  zpnn0elfzo1  10016  ubmelm1fzo  10034  fzoshftral  10046  exbtwnzlemstep  10056  rebtwn2zlemstep  10061  qbtwnrelemcalc  10064  flqaddz  10101  2tnp1ge0ge0  10105  ceiqm1l  10115  qnegmod  10173  addmodlteq  10202  uzsinds  10246  seq3shft2  10277  iseqf1olemab  10293  exp3val  10326  binom2sub1  10437  binom3  10440  zesq  10441  sqoddm1div8  10475  nn0opthlem1d  10498  bcm1k  10538  bcp1n  10539  bcp1m1  10543  bcpasc  10544  bcn2m1  10547  omgadd  10580  hashfz  10599  hashfzo  10600  hashfzp1  10602  zfz1isolemsplit  10613  zfz1isolem1  10615  resqrexlemover  10814  absexpzap  10884  reccn2ap  11114  hashiun  11279  hash2iun1dif1  11281  binomlem  11284  bcxmas  11290  arisum  11299  arisum2  11300  trireciplem  11301  geosergap  11307  pwm1geoserap1  11309  geolim  11312  geolim2  11313  georeclim  11314  geoisum1c  11321  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratnnlemsumlt  11329  cvgratz  11333  mertenslemi1  11336  prodf1f  11344  prodfrecap  11347  ntrivcvgap  11349  prodrbdclem  11372  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  ef0lem  11403  efsub  11424  tanaddaplem  11481  tanaddap  11482  cos01bnd  11501  zeo3  11601  oddm1even  11608  oddp1even  11609  oexpneg  11610  ltoddhalfle  11626  halfleoddlt  11627  nn0ob  11641  flodddiv4  11667  bezoutlema  11723  bezoutlemb  11724  qredeu  11814  oddennn  11941  ennnfonelemp1  11955  dveflem  12895  dvef  12896  reeff1oleme  12901  sin0pilem1  12910  logdivlti  13010  rplogbval  13070  cvgcmp2nlemabs  13402  trilpolemeq1  13408  trilpolemlt1  13409  apdifflemr  13415  iooref1o  13426