Theorem 3cn 12209

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 12192	. 2 ⊢ 3 = (2 + 1)
2		2cn 12203	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11067	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11121	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007  1c1 11010   + caddc 11012  2c2 12183  3c3 12184

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 11067  ax-addcl 11069

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

This theorem is referenced by:  3ex  12210  4cn  12213  4m1e3  12252  3p2e5  12274  3p3e6  12275  4p4e8  12278  5p4e9  12281  3t1e3  12288  3t2e6  12289  3t3e9  12290  8th4div3  12344  halfthird  12345  halfpm6th  12346  6p4e10  12663  9t8e72  12719  sq3  14105  expnass  14115  fac3  14187  01sqrexlem7  15155  caurcvgr  15581  bpoly2  15964  bpoly3  15965  bpoly4  15966  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  cos1bnd  16096  cos2bnd  16097  cos01gt0  16100  rpnnen2lem3  16125  rpnnen2lem11  16133  3dvdsdec  16243  3dvds2dec  16244  5ndvds3  16324  3lcm2e6woprm  16526  prmo3  16953  2exp6  16998  2exp16  17002  7prm  17022  13prm  17027  17prm  17028  19prm  17029  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  tangtx  26412  sincos6thpi  26423  sincos3rdpi  26424  pigt3  26425  pige3ALT  26427  2logb9irrALT  26706  ang180lem2  26718  1cubr  26750  dcubic1lem  26751  dcubic2  26752  dcubic1  26753  dcubic  26754  mcubic  26755  cubic2  26756  cubic  26757  binom4  26758  quart1cl  26762  quart1lem  26763  quart1  26764  quartlem1  26765  quartlem3  26767  log2cnv  26852  log2tlbnd  26853  log2ublem2  26855  log2ublem3  26856  log2ub  26857  basellem5  26993  basellem8  26996  basellem9  26997  cht3  27081  ppiub  27113  chtub  27121  bclbnd  27189  bposlem6  27198  bposlem8  27200  bposlem9  27201  lgsdir2lem1  27234  lgsdir2lem5  27238  2lgslem3b  27306  2lgslem3d  27308  2lgsoddprmlem3c  27321  2lgsoddprmlem3d  27322  addsqnreup  27352  pntibndlem1  27498  pntlemk  27515  ex-opab  30376  ex-exp  30394  ex-dvds  30400  ex-gcd  30401  ex-lcm  30402  ex-prmo  30403  ex-ind-dvds  30405  ply1dg3rt0irred  33519  2sqr3minply  33753  2sqr3nconstr  33754  cos9thpiminplylem2  33756  cos9thpiminplylem3  33757  cos9thpiminplylem4  33758  cos9thpiminplylem5  33759  cos9thpiminply  33761  cos9thpinconstrlem1  33762  cos9thpinconstrlem2  33763  cos9thpinconstr  33764  fib5  34379  fib6  34380  hgt750lem  34625  hgt750lem2  34626  hgt750leme  34632  problem4  35651  problem5  35652  sinccvglem  35655  mblfinlem3  37649  itg2addnclem2  37662  itg2addnclem3  37663  heiborlem6  37806  heiborlem7  37807  3exp7  42036  3lexlogpow2ineq2  42042  3lexlogpow5ineq5  42043  aks4d1p1  42059  2ap1caineq  42128  3rdpwhole  42275  235t711  42288  ex-decpmul  42289  tan3rdpi  42335  sin2t3rdpi  42336  cos2t3rdpi  42337  sin4t3rdpi  42338  cos4t3rdpi  42339  cu3addd  42664  3cubeslem3l  42669  3cubeslem3r  42670  jm2.23  42979  inductionexd  44138  lhe4.4ex1a  44312  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  48342  linevalexample  48390  zlmodzxzequa  48491  zlmodzxzequap  48494  ackval3  48678  ackval2012  48686  ackval3012  48687  ackval41  48690  ackval42  48691