Theorem 1cnd 7972

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7808  1c1 7811

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

This theorem is referenced by:  adddirp1d  7983  muladd11r  8112  recrecap  8665  rec11ap  8666  rec11rap  8667  rerecclap  8686  subrecap  8795  recp1lt1  8855  nn1m1nn  8936  add1p1  9167  sub1m1  9168  cnm2m1cnm3  9169  xp1d2m1eqxm1d2  9170  div4p1lem1div2  9171  peano2z  9288  zaddcllempos  9289  peano2zm  9290  zaddcllemneg  9291  nn0n0n1ge2  9322  zneo  9353  peano5uzti  9360  lincmb01cmp  10002  iccf1o  10003  nnsplit  10136  zpnn0elfzo1  10207  ubmelm1fzo  10225  fzoshftral  10237  exbtwnzlemstep  10247  rebtwn2zlemstep  10252  qbtwnrelemcalc  10255  flqaddz  10296  2tnp1ge0ge0  10300  ceiqm1l  10310  qnegmod  10368  addmodlteq  10397  uzsinds  10441  seq3shft2  10472  iseqf1olemab  10488  exp3val  10521  binom2sub1  10634  binom3  10637  zesq  10638  sqoddm1div8  10673  nn0opthlem1d  10699  bcm1k  10739  bcp1n  10740  bcp1m1  10744  bcpasc  10745  bcn2m1  10748  omgadd  10781  hashfz  10800  hashfzo  10801  hashfzp1  10803  zfz1isolemsplit  10817  zfz1isolem1  10819  resqrexlemover  11018  absexpzap  11088  reccn2ap  11320  hashiun  11485  hash2iun1dif1  11487  binomlem  11490  bcxmas  11496  arisum  11505  arisum2  11506  trireciplem  11507  geosergap  11513  pwm1geoserap1  11515  geolim  11518  geolim2  11519  georeclim  11520  geoisum1c  11527  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratnnlemsumlt  11535  cvgratz  11539  mertenslemi1  11542  prodf1f  11550  prodfrecap  11553  ntrivcvgap  11555  prodrbdclem  11578  prodmodclem3  11582  prodmodclem2a  11583  zproddc  11586  fprodseq  11590  fprodntrivap  11591  prod1dc  11593  fprodmul  11598  prodsnf  11599  fprodsplitdc  11603  fprodm1  11605  fprodp1  11607  fprodcl  11614  fprodfac  11622  fprodrec  11636  fprodclf  11642  ef0lem  11667  efsub  11688  tanaddaplem  11745  tanaddap  11746  cos01bnd  11765  zeo3  11872  oddm1even  11879  oddp1even  11880  oexpneg  11881  ltoddhalfle  11897  halfleoddlt  11898  nn0ob  11912  flodddiv4  11938  bezoutlema  11999  bezoutlemb  12000  uzwodc  12037  qredeu  12096  prmdiv  12234  prmdiveq  12235  pc2dvds  12328  oddennn  12392  ennnfonelemp1  12406  cncrng  13433  dveflem  14157  dvef  14158  reeff1oleme  14163  sin0pilem1  14172  logdivlti  14272  rplogbval  14333  lgsvalmod  14390  lgsdir2  14404  lgsdir  14406  m1lgs  14422  2lgsoddprmlem1  14423  2sqlem8  14440  cvgcmp2nlemabs  14750  iooref1o  14752  trilpolemeq1  14758  trilpolemlt1  14759  apdifflemr  14765  iswomni0  14769  nconstwlpolemgt0  14781