Metamath Proof Explorer

Theorem pnpcan2

Description: Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢A∈ℂ∧C∈ℂ→A+C=C+A
2 1 3adant2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+C=C+A
3 addcom ⊢B∈ℂ∧C∈ℂ→B+C=C+B
4 3 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+C=C+B
5 2 4 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+C-B+C=C+A-C+B
6 pnpcan ⊢C∈ℂ∧A∈ℂ∧B∈ℂ→C+A-C+B=A−B
7 6 3coml ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C+A-C+B=A−B
8 5 7 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+C-B+C=A−B