Metamath Proof Explorer

Theorem nncan

Description: Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion nncan ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − ( 𝐴 − 𝐵 ) ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 subsub2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − ( 𝐴 − 𝐵 ) ) = ( 𝐴 + ( 𝐵 − 𝐴 ) ) )
2 1 3anidm12 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − ( 𝐴 − 𝐵 ) ) = ( 𝐴 + ( 𝐵 − 𝐴 ) ) )
3 pncan3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + ( 𝐵 − 𝐴 ) ) = 𝐵 )
4 2 3 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − ( 𝐴 − 𝐵 ) ) = 𝐵 )