Theorem 3cn 12317

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 12299	. 2 ⊢ 3 = (2 + 1)
2		2cn 12311	. . 3 ⊢ 2 ∈ ℂ
3		ax-1cn 11153	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11210	. 2 ⊢ (2 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093  1c1 11096   + caddc 11098  2c2 12290  3c3 12291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-addcl 11155

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-2 12298  df-3 12299

This theorem is referenced by:  3ex  12318  4cn  12321  4m1e3  12364  3p2e5  12386  3p3e6  12387  4p4e8  12390  5p4e9  12393  3t1e3  12400  3t2e6  12401  2t3e6  12402  3t3e9  12403  8th4div3  12459  halfthird  12460  halfpm6th  12461  6p4e10  12783  9t8e72  12839  sq3  14230  expnass  14240  01sqrexlem7  15295  caurcvgr  15721  bpoly2  16106  bpoly3  16107  bpoly4  16108  ef01bndlem  16235  sin01bnd  16236  cos01bnd  16237  cos1bnd  16238  cos2bnd  16239  cos01gt0  16242  rpnnen2lem3  16267  rpnnen2lem11  16275  3dvdsdec  16385  3dvds2dec  16386  5ndvds3  16466  3lcm2e6woprm  16668  2exp16  17145  13prm  17171  17prm  17172  19prm  17173  37prm  17176  43prm  17177  83prm  17178  139prm  17179  163prm  17180  317prm  17181  631prm  17182  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  1259prm  17191  2503lem1  17192  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  4001prm  17200  tangtx  26670  sincos6thpi  26681  sincos3rdpi  26682  pigt3  26683  pige3ALT  26685  2logb9irrALT  26963  ang180lem2  26975  1cubr  27007  dcubic1lem  27008  dcubic2  27009  dcubic1  27010  dcubic  27011  mcubic  27012  cubic2  27013  cubic  27014  binom4  27015  quart1cl  27019  quart1lem  27020  quart1  27021  quartlem1  27022  quartlem3  27024  log2cnv  27109  log2tlbnd  27110  log2ublem2  27112  log2ublem3  27113  log2ub  27114  basellem5  27249  basellem8  27252  basellem9  27253  ppiub  27368  chtub  27376  bclbnd  27444  bposlem6  27453  bposlem8  27455  bposlem9  27456  lgsdir2lem1  27489  lgsdir2lem5  27493  2lgslem3b  27561  2lgslem3d  27563  2lgsoddprmlem3c  27576  2lgsoddprmlem3d  27577  addsqnreup  27607  pntibndlem1  27753  pntlemk  27770  ex-opab  30783  ex-exp  30801  ex-dvds  30807  ex-gcd  30808  ex-lcm  30809  ex-prmo  30810  ex-ind-dvds  30812  ply1dg3rt0irred  33874  2sqr3minply  34170  2sqr3nconstr  34171  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  cos9thpiminplylem4  34175  cos9thpiminplylem5  34176  cos9thpiminply  34178  cos9thpinconstrlem1  34179  cos9thpinconstrlem2  34180  cos9thpinconstr  34181  fib5  34795  fib6  34796  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  problem4  36160  problem5  36161  sinccvglem  36164  mblfinlem3  38330  itg2addnclem2  38343  itg2addnclem3  38344  heiborlem6  38487  heiborlem7  38488  3lexlogpow2ineq2  42846  3lexlogpow5ineq5  42847  aks4d1p1  42863  2ap1caineq  42932  25or6to4  42993  3rdpwhole  43073  235t711  43086  ex-decpmul  43087  tan3rdpi  43133  sin2t3rdpi  43134  cos2t3rdpi  43135  sin4t3rdpi  43136  cos4t3rdpi  43137  cu3addd  43432  3cubeslem3l  43437  3cubeslem3r  43438  jm2.23  43743  inductionexd  44901  lhe4.4ex1a  45059  stoweidlem13  46747  stoweidlem26  46760  stoweidlem34  46768  wallispilem4  46802  wallispi2lem1  46805  sin5tlem1  47630  sin5tlem2  47631  sin5tlem3  47632  sin5tlem4  47633  sin5tlem5  47634  sin5t  47635  goldrasin  47639  ceil5half3  48103  fmtno5lem1  48325  fmtno5lem2  48326  257prm  48333  fmtno4prmfac  48344  fmtno4nprmfac193  48346  139prmALT  48368  127prm  48371  mod42tp1mod8  48374  3exp4mod41  48388  41prothprmlem2  48390  ppivalnn4  48399  6even  48496  11t31e341  48517  2exp340mod341  48518  gbpart8  48553  sbgoldbwt  48562  sbgoldbst  48563  evengpop3  48583  evengpoap3  48584  nnsum4primeseven  48585  nnsum4primesevenALTV  48586  2t6m3t4e0  49148  linevalexample  49195  zlmodzxzequa  49296  zlmodzxzequap  49299  ackval3  49483  ackval2012  49491  ackval3012  49492  ackval41  49495  ackval42  49496