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