Theorem cnm2m1cnm3

Description: Subtracting 2 and afterwards 1 from a number results in the difference between the number and 3. (Contributed by Alexander van der Vekens, 16-Sep-2018)

	Ref	Expression
Assertion	cnm2m1cnm3	|- ( A e. CC -> ( ( A - 2 ) - 1 ) = ( A - 3 ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( A e. CC -> A e. CC )
2		2cnd	|- ( A e. CC -> 2 e. CC )
3		1cnd	|- ( A e. CC -> 1 e. CC )
4	1 2 3	subsub4d	|- ( A e. CC -> ( ( A - 2 ) - 1 ) = ( A - ( 2 + 1 ) ) )
5		2p1e3	|- ( 2 + 1 ) = 3
6	5	a1i	|- ( A e. CC -> ( 2 + 1 ) = 3 )
7	6	oveq2d	|- ( A e. CC -> ( A - ( 2 + 1 ) ) = ( A - 3 ) )
8	4 7	eqtrd	|- ( A e. CC -> ( ( A - 2 ) - 1 ) = ( A - 3 ) )