Metamath Proof Explorer

Theorem npncan

Description: Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005)

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

Proof

Step Hyp Ref Expression
1 subcl ⊢A∈ℂ∧B∈ℂ→A−B∈ℂ
2 1 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B∈ℂ
3 addsubass ⊢A−B∈ℂ∧B∈ℂ∧C∈ℂ→A−B+B-C=A−B+B-C
4 2 3 syld3an1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B+B-C=A−B+B-C
5 npcan ⊢A∈ℂ∧B∈ℂ→A-B+B=A
6 5 oveq1d ⊢A∈ℂ∧B∈ℂ→A−B+B-C=A−C
7 6 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B+B-C=A−C
8 4 7 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B+B-C=A−C