Metamath Proof Explorer

Theorem nppcan2

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

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

Proof

Step Hyp Ref Expression
1 addcl ⊢B∈ℂ∧C∈ℂ→B+C∈ℂ
2 1 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+C∈ℂ
3 subsub ⊢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 pncan ⊢B∈ℂ∧C∈ℂ→B+C-C=B
6 5 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+C-C=B
7 6 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B+C-C=A−B
8 4 7 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A-B+C+C=A−B