Theorem 9m1e8

Description: 9 - 1 = 8. (Contributed by AV, 6-Sep-2021)

	Ref	Expression
Assertion	9m1e8	⊢ ( 9 − 1 ) = 8

Proof

Step	Hyp	Ref	Expression
1		8cn	⊢ 8 ∈ ℂ
2		ax-1cn	⊢ 1 ∈ ℂ
3		df-9	⊢ 9 = ( 8 + 1 )
4	1 2 3	mvrraddi	⊢ ( 9 − 1 ) = 8