Theorem 3cn 12238

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 12221	. 2 ⊢ 3 = (2 + 1)
2		2cn 12232	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11150	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   + caddc 11041  2c2 12212  3c3 12213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12220  df-3 12221

This theorem is referenced by:  3ex  12239  4cn  12242  4m1e3  12281  3p2e5  12303  3p3e6  12304  4p4e8  12307  5p4e9  12310  3t1e3  12317  3t2e6  12318  3t3e9  12319  8th4div3  12373  halfthird  12374  halfpm6th  12375  6p4e10  12691  9t8e72  12747  sq3  14133  expnass  14143  fac3  14215  01sqrexlem7  15183  caurcvgr  15609  bpoly2  15992  bpoly3  15993  bpoly4  15994  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  cos1bnd  16124  cos2bnd  16125  cos01gt0  16128  rpnnen2lem3  16153  rpnnen2lem11  16161  3dvdsdec  16271  3dvds2dec  16272  5ndvds3  16352  3lcm2e6woprm  16554  prmo3  16981  2exp6  17026  2exp16  17030  7prm  17050  13prm  17055  17prm  17056  19prm  17057  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  tangtx  26485  sincos6thpi  26496  sincos3rdpi  26497  pigt3  26498  pige3ALT  26500  2logb9irrALT  26779  ang180lem2  26791  1cubr  26823  dcubic1lem  26824  dcubic2  26825  dcubic1  26826  dcubic  26827  mcubic  26828  cubic2  26829  cubic  26830  binom4  26831  quart1cl  26835  quart1lem  26836  quart1  26837  quartlem1  26838  quartlem3  26840  log2cnv  26925  log2tlbnd  26926  log2ublem2  26928  log2ublem3  26929  log2ub  26930  basellem5  27066  basellem8  27069  basellem9  27070  cht3  27154  ppiub  27186  chtub  27194  bclbnd  27262  bposlem6  27271  bposlem8  27273  bposlem9  27274  lgsdir2lem1  27307  lgsdir2lem5  27311  2lgslem3b  27379  2lgslem3d  27381  2lgsoddprmlem3c  27394  2lgsoddprmlem3d  27395  addsqnreup  27425  pntibndlem1  27571  pntlemk  27588  ex-opab  30523  ex-exp  30541  ex-dvds  30547  ex-gcd  30548  ex-lcm  30549  ex-prmo  30550  ex-ind-dvds  30552  ply1dg3rt0irred  33681  2sqr3minply  33962  2sqr3nconstr  33963  cos9thpiminplylem2  33965  cos9thpiminplylem3  33966  cos9thpiminplylem4  33967  cos9thpiminplylem5  33968  cos9thpiminply  33970  cos9thpinconstrlem1  33971  cos9thpinconstrlem2  33972  cos9thpinconstr  33973  fib5  34587  fib6  34588  hgt750lem  34833  hgt750lem2  34834  hgt750leme  34840  problem4  35888  problem5  35889  sinccvglem  35892  mblfinlem3  37914  itg2addnclem2  37927  itg2addnclem3  37928  heiborlem6  38071  heiborlem7  38072  3exp7  42427  3lexlogpow2ineq2  42433  3lexlogpow5ineq5  42434  aks4d1p1  42450  2ap1caineq  42519  3rdpwhole  42666  235t711  42679  ex-decpmul  42680  tan3rdpi  42726  sin2t3rdpi  42727  cos2t3rdpi  42728  sin4t3rdpi  42729  cos4t3rdpi  42730  cu3addd  43042  3cubeslem3l  43047  3cubeslem3r  43048  jm2.23  43357  inductionexd  44515  lhe4.4ex1a  44689  stoweidlem13  46375  stoweidlem26  46388  stoweidlem34  46396  wallispilem4  46430  wallispi2lem1  46433  ceil5half3  47704  fmtno5lem1  47917  fmtno5lem2  47918  257prm  47925  fmtno4prmfac  47936  fmtno4nprmfac193  47938  139prmALT  47960  127prm  47963  mod42tp1mod8  47966  3exp4mod41  47980  41prothprmlem2  47982  6even  48075  11t31e341  48096  2exp340mod341  48097  gbpart8  48132  sbgoldbwt  48141  sbgoldbst  48142  evengpop3  48162  evengpoap3  48163  nnsum4primeseven  48164  nnsum4primesevenALTV  48165  2t6m3t4e0  48712  linevalexample  48759  zlmodzxzequa  48860  zlmodzxzequap  48863  ackval3  49047  ackval2012  49055  ackval3012  49056  ackval41  49059  ackval42  49060