Theorem 3p2e5

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

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

Proof

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$$