Theorem 1cnd 8042

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7877  1c1 7880

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

This theorem is referenced by:  adddirp1d  8053  muladd11r  8182  muls1d  8444  recrecap  8736  rec11ap  8737  rec11rap  8738  rerecclap  8757  subrecap  8866  recp1lt1  8926  nn1m1nn  9008  add1p1  9241  sub1m1  9242  cnm2m1cnm3  9243  xp1d2m1eqxm1d2  9244  div4p1lem1div2  9245  peano2z  9362  zaddcllempos  9363  peano2zm  9364  zaddcllemneg  9365  nn0n0n1ge2  9396  zneo  9427  peano5uzti  9434  lincmb01cmp  10078  iccf1o  10079  nnsplit  10212  zpnn0elfzo1  10284  ubmelm1fzo  10302  fzoshftral  10314  exbtwnzlemstep  10337  rebtwn2zlemstep  10342  qbtwnrelemcalc  10345  flqaddz  10387  2tnp1ge0ge0  10391  ceiqm1l  10403  qnegmod  10461  addmodlteq  10490  uzsinds  10536  seq3shft2  10573  iseqf1olemab  10594  exp3val  10633  binom2sub1  10746  binom3  10749  zesq  10750  sqoddm1div8  10785  nn0opthlem1d  10812  bcm1k  10852  bcp1n  10853  bcp1m1  10857  bcpasc  10858  bcn2m1  10861  omgadd  10894  hashfz  10913  hashfzo  10914  hashfzp1  10916  zfz1isolemsplit  10930  zfz1isolem1  10932  resqrexlemover  11175  absexpzap  11245  reccn2ap  11478  hashiun  11643  hash2iun1dif1  11645  binomlem  11648  bcxmas  11654  arisum  11663  arisum2  11664  trireciplem  11665  geosergap  11671  pwm1geoserap1  11673  geolim  11676  geolim2  11677  georeclim  11678  geoisum1c  11685  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemsumlt  11693  cvgratz  11697  mertenslemi1  11700  prodf1f  11708  prodfrecap  11711  ntrivcvgap  11713  prodrbdclem  11736  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodntrivap  11749  prod1dc  11751  fprodmul  11756  prodsnf  11757  fprodsplitdc  11761  fprodm1  11763  fprodp1  11765  fprodcl  11772  fprodfac  11780  fprodrec  11794  fprodclf  11800  ef0lem  11825  efsub  11846  tanaddaplem  11903  tanaddap  11904  cos01bnd  11923  zeo3  12033  oddm1even  12040  oddp1even  12041  oexpneg  12042  ltoddhalfle  12058  halfleoddlt  12059  nn0ob  12073  flodddiv4  12101  bitsp1o  12117  bezoutlema  12166  bezoutlemb  12167  uzwodc  12204  qredeu  12265  prmdiv  12403  prmdiveq  12404  pc2dvds  12499  4sqlem11  12570  4sqlem12  12571  oddennn  12609  ennnfonelemp1  12623  gsumfzconst  13471  cncrng  14125  expcn  14805  hoverb  14884  dveflem  14962  dvef  14963  dvply2g  15002  reeff1oleme  15008  sin0pilem1  15017  logdivlti  15117  rpcxpmul2  15149  rplogbval  15181  perfectlem2  15236  lgsvalmod  15260  lgsdir2  15274  lgsdir  15276  gausslemma2dlem1a  15299  gausslemma2dlem5  15307  lgseisenlem4  15314  lgsquadlem1  15318  m1lgs  15326  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgslem3d1  15341  2lgsoddprmlem1  15346  2sqlem8  15364  cvgcmp2nlemabs  15676  iooref1o  15678  trilpolemeq1  15684  trilpolemlt1  15685  apdifflemr  15691  iswomni0  15695  nconstwlpolemgt0  15708