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 ∈ ℂ → A + 1 - 1 = A

Proof

Step Hyp Ref Expression
1 id ⊢ A ∈ ℂ → A ∈ ℂ
2 1cnd ⊢ A ∈ ℂ → 1 ∈ ℂ
3 1 2 pncand ⊢ A ∈ ℂ → A + 1 - 1 = A