Theorem 3cn 12243

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 12226	. 2 ⊢ 3 = (2 + 1)
2		2cn 12237	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11102	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11156	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042  1c1 11045   + caddc 11047  2c2 12217  3c3 12218

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12225  df-3 12226

This theorem is referenced by:  3ex  12244  4cn  12247  4m1e3  12286  3p2e5  12308  3p3e6  12309  4p4e8  12312  5p4e9  12315  3t1e3  12322  3t2e6  12323  3t3e9  12324  8th4div3  12378  halfthird  12379  halfpm6th  12380  6p4e10  12697  9t8e72  12753  sq3  14139  expnass  14149  fac3  14221  01sqrexlem7  15190  caurcvgr  15616  bpoly2  15999  bpoly3  16000  bpoly4  16001  ef01bndlem  16128  sin01bnd  16129  cos01bnd  16130  cos1bnd  16131  cos2bnd  16132  cos01gt0  16135  rpnnen2lem3  16160  rpnnen2lem11  16168  3dvdsdec  16278  3dvds2dec  16279  5ndvds3  16359  3lcm2e6woprm  16561  prmo3  16988  2exp6  17033  2exp16  17037  7prm  17057  13prm  17062  17prm  17063  19prm  17064  37prm  17067  43prm  17068  83prm  17069  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  tangtx  26447  sincos6thpi  26458  sincos3rdpi  26459  pigt3  26460  pige3ALT  26462  2logb9irrALT  26741  ang180lem2  26753  1cubr  26785  dcubic1lem  26786  dcubic2  26787  dcubic1  26788  dcubic  26789  mcubic  26790  cubic2  26791  cubic  26792  binom4  26793  quart1cl  26797  quart1lem  26798  quart1  26799  quartlem1  26800  quartlem3  26802  log2cnv  26887  log2tlbnd  26888  log2ublem2  26890  log2ublem3  26891  log2ub  26892  basellem5  27028  basellem8  27031  basellem9  27032  cht3  27116  ppiub  27148  chtub  27156  bclbnd  27224  bposlem6  27233  bposlem8  27235  bposlem9  27236  lgsdir2lem1  27269  lgsdir2lem5  27273  2lgslem3b  27341  2lgslem3d  27343  2lgsoddprmlem3c  27356  2lgsoddprmlem3d  27357  addsqnreup  27387  pntibndlem1  27533  pntlemk  27550  ex-opab  30411  ex-exp  30429  ex-dvds  30435  ex-gcd  30436  ex-lcm  30437  ex-prmo  30438  ex-ind-dvds  30440  ply1dg3rt0irred  33544  2sqr3minply  33763  2sqr3nconstr  33764  cos9thpiminplylem2  33766  cos9thpiminplylem3  33767  cos9thpiminplylem4  33768  cos9thpiminplylem5  33769  cos9thpiminply  33771  cos9thpinconstrlem1  33772  cos9thpinconstrlem2  33773  cos9thpinconstr  33774  fib5  34389  fib6  34390  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  problem4  35648  problem5  35649  sinccvglem  35652  mblfinlem3  37646  itg2addnclem2  37659  itg2addnclem3  37660  heiborlem6  37803  heiborlem7  37804  3exp7  42034  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1  42057  2ap1caineq  42126  3rdpwhole  42273  235t711  42286  ex-decpmul  42287  tan3rdpi  42333  sin2t3rdpi  42334  cos2t3rdpi  42335  sin4t3rdpi  42336  cos4t3rdpi  42337  cu3addd  42662  3cubeslem3l  42667  3cubeslem3r  42668  jm2.23  42978  inductionexd  44137  lhe4.4ex1a  44311  stoweidlem13  46004  stoweidlem26  46017  stoweidlem34  46025  wallispilem4  46059  wallispi2lem1  46062  ceil5half3  47334  fmtno5lem1  47547  fmtno5lem2  47548  257prm  47555  fmtno4prmfac  47566  fmtno4nprmfac193  47568  139prmALT  47590  127prm  47593  mod42tp1mod8  47596  3exp4mod41  47610  41prothprmlem2  47612  6even  47705  11t31e341  47726  2exp340mod341  47727  gbpart8  47762  sbgoldbwt  47771  sbgoldbst  47772  evengpop3  47792  evengpoap3  47793  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  2t6m3t4e0  48329  linevalexample  48377  zlmodzxzequa  48478  zlmodzxzequap  48481  ackval3  48665  ackval2012  48673  ackval3012  48674  ackval41  48677  ackval42  48678