Metamath Proof Explorer

Theorem nppcan3

Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 subcl ⊢A∈ℂ∧B∈ℂ→A−B∈ℂ
2 1 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B∈ℂ
3 simp3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C∈ℂ
4 simp2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B∈ℂ
5 2 3 4 addassd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B+C+B=A−B+C+B
6 nppcan ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B+C+B=A+C
7 5 6 eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B+C+B=A+C