Theorem 8p1e9

Description: 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015)

	Ref	Expression
Assertion	8p1e9	$$⊢8+1=9$$

Proof

Step	Hyp	Ref	Expression
1		df-9	$$⊢9=8+1$$
2	1	eqcomi	$$⊢8+1=9$$