Theorem 3cn 12226

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 12209	. 2 ⊢ 3 = (2 + 1)
2		2cn 12220	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11138	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   + caddc 11029  2c2 12200  3c3 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-2 12208  df-3 12209

This theorem is referenced by:  3ex  12227  4cn  12230  4m1e3  12269  3p2e5  12291  3p3e6  12292  4p4e8  12295  5p4e9  12298  3t1e3  12305  3t2e6  12306  3t3e9  12307  8th4div3  12361  halfthird  12362  halfpm6th  12363  6p4e10  12679  9t8e72  12735  sq3  14121  expnass  14131  fac3  14203  01sqrexlem7  15171  caurcvgr  15597  bpoly2  15980  bpoly3  15981  bpoly4  15982  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  cos1bnd  16112  cos2bnd  16113  cos01gt0  16116  rpnnen2lem3  16141  rpnnen2lem11  16149  3dvdsdec  16259  3dvds2dec  16260  5ndvds3  16340  3lcm2e6woprm  16542  prmo3  16969  2exp6  17014  2exp16  17018  7prm  17038  13prm  17043  17prm  17044  19prm  17045  37prm  17048  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  tangtx  26470  sincos6thpi  26481  sincos3rdpi  26482  pigt3  26483  pige3ALT  26485  2logb9irrALT  26764  ang180lem2  26776  1cubr  26808  dcubic1lem  26809  dcubic2  26810  dcubic1  26811  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  binom4  26816  quart1cl  26820  quart1lem  26821  quart1  26822  quartlem1  26823  quartlem3  26825  log2cnv  26910  log2tlbnd  26911  log2ublem2  26913  log2ublem3  26914  log2ub  26915  basellem5  27051  basellem8  27054  basellem9  27055  cht3  27139  ppiub  27171  chtub  27179  bclbnd  27247  bposlem6  27256  bposlem8  27258  bposlem9  27259  lgsdir2lem1  27292  lgsdir2lem5  27296  2lgslem3b  27364  2lgslem3d  27366  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  addsqnreup  27410  pntibndlem1  27556  pntlemk  27573  ex-opab  30507  ex-exp  30525  ex-dvds  30531  ex-gcd  30532  ex-lcm  30533  ex-prmo  30534  ex-ind-dvds  30536  ply1dg3rt0irred  33665  2sqr3minply  33937  2sqr3nconstr  33938  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminplylem4  33942  cos9thpiminplylem5  33943  cos9thpiminply  33945  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  cos9thpinconstr  33948  fib5  34562  fib6  34563  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  problem4  35862  problem5  35863  sinccvglem  35866  mblfinlem3  37860  itg2addnclem2  37873  itg2addnclem3  37874  heiborlem6  38017  heiborlem7  38018  3exp7  42317  3lexlogpow2ineq2  42323  3lexlogpow5ineq5  42324  aks4d1p1  42340  2ap1caineq  42409  3rdpwhole  42557  235t711  42570  ex-decpmul  42571  tan3rdpi  42617  sin2t3rdpi  42618  cos2t3rdpi  42619  sin4t3rdpi  42620  cos4t3rdpi  42621  cu3addd  42933  3cubeslem3l  42938  3cubeslem3r  42939  jm2.23  43248  inductionexd  44406  lhe4.4ex1a  44580  stoweidlem13  46267  stoweidlem26  46280  stoweidlem34  46288  wallispilem4  46322  wallispi2lem1  46325  ceil5half3  47596  fmtno5lem1  47809  fmtno5lem2  47810  257prm  47817  fmtno4prmfac  47828  fmtno4nprmfac193  47830  139prmALT  47852  127prm  47855  mod42tp1mod8  47858  3exp4mod41  47872  41prothprmlem2  47874  6even  47967  11t31e341  47988  2exp340mod341  47989  gbpart8  48024  sbgoldbwt  48033  sbgoldbst  48034  evengpop3  48054  evengpoap3  48055  nnsum4primeseven  48056  nnsum4primesevenALTV  48057  2t6m3t4e0  48604  linevalexample  48651  zlmodzxzequa  48752  zlmodzxzequap  48755  ackval3  48939  ackval2012  48947  ackval3012  48948  ackval41  48951  ackval42  48952