Theorem 6p2e8

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

	Ref	Expression
Assertion	6p2e8	$$⊢6+2=8$$

Proof

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