Theorem 2cn

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022)

	Ref	Expression
Assertion	2cn	|- 2 e. CC

Proof

Step	Hyp	Ref	Expression
1		df-2	|- 2 = ( 1 + 1 )
2		ax-1cn	|- 1 e. CC
3	2 2	addcli	|- ( 1 + 1 ) e. CC
4	1 3	eqeltri	|- 2 e. CC