This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 10m1e9

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

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

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$