Theorem 3m1e2

Description: 3 - 1 = 2. (Contributed by FL, 17-Oct-2010) (Revised by NM, 10-Dec-2017) (Proof shortened by AV, 6-Sep-2021)

	Ref	Expression
Assertion	3m1e2	⊢ ( 3 − 1 ) = 2

Proof

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