Theorem 3cn 8698

Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)

Assertion

Ref	Expression
3cn	|- 3 e. CC

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		3re 8697	. 2 |- 3 e. RR
2	1	recni 7695	1 |- 3 e. CC

Syntax hints:   e. wcel 1461   CCcc 7538   3c3 8675

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-resscn 7630  ax-1re 7632  ax-addrcl 7635

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-in 3041  df-ss 3048  df-2 8682  df-3 8683

This theorem is referenced by:  3ex  8699  3m1e2  8743  3p2e5  8758  3p3e6  8759  4p4e8  8762  5p4e9  8765  3t1e3  8772  3t2e6  8773  3t3e9  8774  8th4div3  8836  halfpm6th  8837  6p4e10  9150  9t8e72  9206  fzo0to42pr  9883  sq3  10275  expnass  10284  fac3  10364  4bc3eq4  10405  ef01bndlem  11307  sin01bnd  11308  cos01bnd  11309  cos1bnd  11310  cos2bnd  11311  cos01gt0  11313  3dvdsdec  11403  3dvds2dec  11404  3lcm2e6woprm  11606  ex-exp  12619  ex-dvds  12622  ex-gcd  12623