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

Metamath Proof Explorer

Theorem 3p2e5

Description: 3 + 2 = 5. (Contributed by NM, 11-May-2004)

		Ref	Expression
	Assertion	3p2e5	$⊢ 3 + 2 = 5$

Step	Hyp	Ref	Expression
1		df-2	$⊢ 2 = 1 + 1$
2	1	oveq2i	$⊢ 3 + 2 = 3 + 1 + 1$
3		3cn	$⊢ 3 \in ℂ$
4		ax-1cn	$⊢ 1 \in ℂ$
5	3 4 4	addassi	$⊢ 3 + 1 + 1 = 3 + 1 + 1$
6	2 5	eqtr4i	$⊢ 3 + 2 = 3 + 1 + 1$
7		df-4	$⊢ 4 = 3 + 1$
8	7	oveq1i	$⊢ 4 + 1 = 3 + 1 + 1$
9	6 8	eqtr4i	$⊢ 3 + 2 = 4 + 1$
10		df-5	$⊢ 5 = 4 + 1$
11	9 10	eqtr4i	$⊢ 3 + 2 = 5$