Theorem 7p2e9

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

	Ref	Expression
Assertion	7p2e9	$$⊢7+2=9$$

Proof

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