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  33518  2sqr3minply  33747  2sqr3nconstr  33748  cos9thpiminplylem2  33750  cos9thpiminplylem3  33751  cos9thpiminplylem4  33752  cos9thpiminplylem5  33753  cos9thpiminply  33755  cos9thpinconstrlem1  33756  cos9thpinconstrlem2  33757  cos9thpinconstr  33758  fib5  34373  fib6  34374  hgt750lem  34619  hgt750lem2  34620  hgt750leme  34626  problem4  35645  problem5  35646  sinccvglem  35649  mblfinlem3  37643  itg2addnclem2  37656  itg2addnclem3  37657  heiborlem6  37800  heiborlem7  37801  3exp7  42030  3lexlogpow2ineq2  42036  3lexlogpow5ineq5  42037  aks4d1p1  42053  2ap1caineq  42122  3rdpwhole  42269  235t711  42282  ex-decpmul  42283  tan3rdpi  42329  sin2t3rdpi  42330  cos2t3rdpi  42331  sin4t3rdpi  42332  cos4t3rdpi  42333  cu3addd  42658  3cubeslem3l  42663  3cubeslem3r  42664  jm2.23  42973  inductionexd  44132  lhe4.4ex1a  44306  stoweidlem13  45998  stoweidlem26  46011  stoweidlem34  46019  wallispilem4  46053  wallispi2lem1  46056  ceil5half3  47328  fmtno5lem1  47541  fmtno5lem2  47542  257prm  47549  fmtno4prmfac  47560  fmtno4nprmfac193  47562  139prmALT  47584  127prm  47587  mod42tp1mod8  47590  3exp4mod41  47604  41prothprmlem2  47606  6even  47699  11t31e341  47720  2exp340mod341  47721  gbpart8  47756  sbgoldbwt  47765  sbgoldbst  47766  evengpop3  47786  evengpoap3  47787  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  2t6m3t4e0  48336  linevalexample  48384  zlmodzxzequa  48485  zlmodzxzequap  48488  ackval3  48672  ackval2012  48680  ackval3012  48681  ackval41  48684  ackval42  48685