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\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2		ax-1cn	$$⊢1\in ℂ$$
3	2 2	addcli	$$⊢1+1\in ℂ$$
4	1 3	eqeltri	$$⊢2\in ℂ$$