Theorem 3cn 8114

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 8113	. 2 |- 3 e. RR
2	1	recni 7131	1 |- 3 e. CC

Syntax hints:   e. wcel 1433   CCcc 6979   3c3 8090

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068  ax-1re 7070  ax-addrcl 7073

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986  df-2 8098  df-3 8099

This theorem is referenced by:  3ex  8115  3m1e2  8158  3p2e5  8173  3p3e6  8174  4p4e8  8177  5p4e9  8180  3t1e3  8187  3t2e6  8188  3t3e9  8189  8th4div3  8250  halfpm6th  8251  6p4e10  8548  9t8e72  8604  fzo0to42pr  9229  sq3  9572  expnass  9580  fac3  9659  4bc3eq4  9700  3dvdsdec  10264  3dvds2dec  10265  3lcm2e6woprm  10468  ex-dvds  10567  ex-gcd  10568