Metamath Proof Explorer

Theorem pncan1

Description: Cancellation law for addition and subtraction with 1. (Contributed by Alexander van der Vekens, 3-Oct-2018)

Ref Expression
Assertion pncan1 
|- ( A e. CC -> ( ( A + 1 ) - 1 ) = A )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. CC -> A e. CC )
2 1cnd 
 |-  ( A e. CC -> 1 e. CC )
3 1 2 pncand 
 |-  ( A e. CC -> ( ( A + 1 ) - 1 ) = A )