Theorem 4p2e6

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

	Ref	Expression
Assertion	4p2e6	$$⊢4+2=6$$

Proof

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