Theorem 5p2e7

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

	Ref	Expression
Assertion	5p2e7	$$⊢5+2=7$$

Proof

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