Metamath Proof Explorer

Theorem nnncan1

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

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

Proof

Step Hyp Ref Expression
1 subcl ⊢A∈ℂ∧C∈ℂ→A−C∈ℂ
2 1 3adant2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−C∈ℂ
3 sub32 ⊢A∈ℂ∧B∈ℂ∧A−C∈ℂ→A-B-A−C=A-A−C-B
4 2 3 syld3an3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-B-A−C=A-A−C-B
5 nncan ⊢A∈ℂ∧C∈ℂ→A−A−C=C
6 5 3adant2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−A−C=C
7 6 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-A−C-B=C−B
8 4 7 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-B-A−C=C−B