Metamath Proof Explorer


Theorem npcan1

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

Ref Expression
Assertion npcan1 A A - 1 + 1 = A

Proof

Step Hyp Ref Expression
1 id A A
2 1cnd A 1
3 1 2 npcand A A - 1 + 1 = A