Theorem 3cn 12347

Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
3cn	⊢ 3 ∈ ℂ

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		df-3 12330	. 2 ⊢ 3 = (2 + 1)
2		2cn 12341	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11213	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11267	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2837	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   + caddc 11158  2c2 12321  3c3 12322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-2 12329  df-3 12330

This theorem is referenced by:  3ex  12348  4cn  12351  4m1e3  12395  3p2e5  12417  3p3e6  12418  4p4e8  12421  5p4e9  12424  3t1e3  12431  3t2e6  12432  3t3e9  12433  8th4div3  12486  halfpm6th  12487  6p4e10  12805  9t8e72  12861  halfthird  12876  sq3  14237  expnass  14247  fac3  14319  01sqrexlem7  15287  caurcvgr  15710  bpoly2  16093  bpoly3  16094  bpoly4  16095  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  cos1bnd  16223  cos2bnd  16224  cos01gt0  16227  rpnnen2lem3  16252  rpnnen2lem11  16260  3dvdsdec  16369  3dvds2dec  16370  5ndvds3  16450  3lcm2e6woprm  16652  prmo3  17079  2exp6  17124  2exp16  17128  7prm  17148  13prm  17153  17prm  17154  19prm  17155  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  tangtx  26547  sincos6thpi  26558  sincos3rdpi  26559  pigt3  26560  pige3ALT  26562  2logb9irrALT  26841  ang180lem2  26853  1cubr  26885  dcubic1lem  26886  dcubic2  26887  dcubic1  26888  dcubic  26889  mcubic  26890  cubic2  26891  cubic  26892  binom4  26893  quart1cl  26897  quart1lem  26898  quart1  26899  quartlem1  26900  quartlem3  26902  log2cnv  26987  log2tlbnd  26988  log2ublem2  26990  log2ublem3  26991  log2ub  26992  basellem5  27128  basellem8  27131  basellem9  27132  cht3  27216  ppiub  27248  chtub  27256  bclbnd  27324  bposlem6  27333  bposlem8  27335  bposlem9  27336  lgsdir2lem1  27369  lgsdir2lem5  27373  2lgslem3b  27441  2lgslem3d  27443  2lgsoddprmlem3c  27456  2lgsoddprmlem3d  27457  addsqnreup  27487  pntibndlem1  27633  pntlemk  27650  ex-opab  30451  ex-exp  30469  ex-dvds  30475  ex-gcd  30476  ex-lcm  30477  ex-prmo  30478  ex-ind-dvds  30480  ply1dg3rt0irred  33607  2sqr3minply  33791  fib5  34407  fib6  34408  hgt750lem  34666  hgt750lem2  34667  hgt750leme  34673  problem4  35673  problem5  35674  sinccvglem  35677  mblfinlem3  37666  itg2addnclem2  37679  itg2addnclem3  37680  heiborlem6  37823  heiborlem7  37824  3exp7  42054  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1p1  42077  2ap1caineq  42146  fac2xp3  42240  235t711  42339  ex-decpmul  42340  tan3rdpi  42386  cu3addd  42691  3cubeslem3l  42697  3cubeslem3r  42698  jm2.23  43008  inductionexd  44168  lhe4.4ex1a  44348  stoweidlem13  46028  stoweidlem26  46041  stoweidlem34  46049  wallispilem4  46083  wallispi2lem1  46086  ceil5half3  47342  fmtno5lem1  47540  fmtno5lem2  47541  257prm  47548  fmtno4prmfac  47559  fmtno4nprmfac193  47561  139prmALT  47583  127prm  47586  mod42tp1mod8  47589  3exp4mod41  47603  41prothprmlem2  47605  6even  47698  11t31e341  47719  2exp340mod341  47720  gbpart8  47755  sbgoldbwt  47764  sbgoldbst  47765  evengpop3  47785  evengpoap3  47786  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  2t6m3t4e0  48264  linevalexample  48312  zlmodzxzequa  48413  zlmodzxzequap  48416  ackval3  48604  ackval2012  48612  ackval3012  48613  ackval41  48616  ackval42  48617