This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3cn

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)

		Ref	Expression
	Assertion	3cn	$⊢ 3 \in ℂ$

Proof

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