Metamath Proof Explorer

Theorem nnncan

Description: Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005)

Ref Expression
Assertion nnncan ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-B−C-C=A−B

Proof

Step Hyp Ref Expression
1 subcl ⊢B∈ℂ∧C∈ℂ→B−C∈ℂ
2 1 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B−C∈ℂ
3 subsub4 ⊢A∈ℂ∧B−C∈ℂ∧C∈ℂ→A-B−C-C=A−B-C+C
4 2 3 syld3an2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-B−C-C=A−B-C+C
5 npcan ⊢B∈ℂ∧C∈ℂ→B-C+C=B
6 5 oveq2d ⊢B∈ℂ∧C∈ℂ→A−B-C+C=A−B
7 6 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B-C+C=A−B
8 4 7 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-B−C-C=A−B