Theorem 1e2m1

Description: 1 = 2 - 1. (Contributed by David A. Wheeler, 8-Dec-2018)

	Ref	Expression
Assertion	1e2m1	⊢ 1 = ( 2 − 1 )

Proof

Step	Hyp	Ref	Expression
1		2m1e1	⊢ ( 2 − 1 ) = 1
2	1	eqcomi	⊢ 1 = ( 2 − 1 )