Theorem 3cn 12274

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 12257	. 2 ⊢ 3 = (2 + 1)
2		2cn 12268	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11133	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11187	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   + caddc 11078  2c2 12248  3c3 12249

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 2702  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-2 12256  df-3 12257

This theorem is referenced by:  3ex  12275  4cn  12278  4m1e3  12317  3p2e5  12339  3p3e6  12340  4p4e8  12343  5p4e9  12346  3t1e3  12353  3t2e6  12354  3t3e9  12355  8th4div3  12409  halfthird  12410  halfpm6th  12411  6p4e10  12728  9t8e72  12784  sq3  14170  expnass  14180  fac3  14252  01sqrexlem7  15221  caurcvgr  15647  bpoly2  16030  bpoly3  16031  bpoly4  16032  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  cos1bnd  16162  cos2bnd  16163  cos01gt0  16166  rpnnen2lem3  16191  rpnnen2lem11  16199  3dvdsdec  16309  3dvds2dec  16310  5ndvds3  16390  3lcm2e6woprm  16592  prmo3  17019  2exp6  17064  2exp16  17068  7prm  17088  13prm  17093  17prm  17094  19prm  17095  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  tangtx  26421  sincos6thpi  26432  sincos3rdpi  26433  pigt3  26434  pige3ALT  26436  2logb9irrALT  26715  ang180lem2  26727  1cubr  26759  dcubic1lem  26760  dcubic2  26761  dcubic1  26762  dcubic  26763  mcubic  26764  cubic2  26765  cubic  26766  binom4  26767  quart1cl  26771  quart1lem  26772  quart1  26773  quartlem1  26774  quartlem3  26776  log2cnv  26861  log2tlbnd  26862  log2ublem2  26864  log2ublem3  26865  log2ub  26866  basellem5  27002  basellem8  27005  basellem9  27006  cht3  27090  ppiub  27122  chtub  27130  bclbnd  27198  bposlem6  27207  bposlem8  27209  bposlem9  27210  lgsdir2lem1  27243  lgsdir2lem5  27247  2lgslem3b  27315  2lgslem3d  27317  2lgsoddprmlem3c  27330  2lgsoddprmlem3d  27331  addsqnreup  27361  pntibndlem1  27507  pntlemk  27524  ex-opab  30368  ex-exp  30386  ex-dvds  30392  ex-gcd  30393  ex-lcm  30394  ex-prmo  30395  ex-ind-dvds  30397  ply1dg3rt0irred  33558  2sqr3minply  33777  2sqr3nconstr  33778  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  cos9thpiminply  33785  cos9thpinconstrlem1  33786  cos9thpinconstrlem2  33787  cos9thpinconstr  33788  fib5  34403  fib6  34404  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  problem4  35662  problem5  35663  sinccvglem  35666  mblfinlem3  37660  itg2addnclem2  37673  itg2addnclem3  37674  heiborlem6  37817  heiborlem7  37818  3exp7  42048  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1  42071  2ap1caineq  42140  3rdpwhole  42287  235t711  42300  ex-decpmul  42301  tan3rdpi  42347  sin2t3rdpi  42348  cos2t3rdpi  42349  sin4t3rdpi  42350  cos4t3rdpi  42351  cu3addd  42676  3cubeslem3l  42681  3cubeslem3r  42682  jm2.23  42992  inductionexd  44151  lhe4.4ex1a  44325  stoweidlem13  46018  stoweidlem26  46031  stoweidlem34  46039  wallispilem4  46073  wallispi2lem1  46076  ceil5half3  47345  fmtno5lem1  47558  fmtno5lem2  47559  257prm  47566  fmtno4prmfac  47577  fmtno4nprmfac193  47579  139prmALT  47601  127prm  47604  mod42tp1mod8  47607  3exp4mod41  47621  41prothprmlem2  47623  6even  47716  11t31e341  47737  2exp340mod341  47738  gbpart8  47773  sbgoldbwt  47782  sbgoldbst  47783  evengpop3  47803  evengpoap3  47804  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  2t6m3t4e0  48340  linevalexample  48388  zlmodzxzequa  48489  zlmodzxzequap  48492  ackval3  48676  ackval2012  48684  ackval3012  48685  ackval41  48688  ackval42  48689