Theorem 10m1e9

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

	Ref	Expression
Assertion	10m1e9	$$⊢10-1=9$$

Proof

Step	Hyp	Ref	Expression
1		9cn	$$⊢9\in ℂ$$
2		ax-1cn	$$⊢1\in ℂ$$
3		9p1e10	$$⊢9+1=10$$
4	3	eqcomi	$$⊢10=9+1$$
5	1 2 4	mvrraddi	$$⊢10-1=9$$