Metamath Proof Explorer

Theorem ppncan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢A∈ℂ∧B∈ℂ→A+B=B+A
2 1 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B=B+A
3 2 oveq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B-B−C=B+A-B−C
4 addcl ⊢A∈ℂ∧B∈ℂ→A+B∈ℂ
5 4 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B∈ℂ
6 subsub2 ⊢A+B∈ℂ∧B∈ℂ∧C∈ℂ→A+B-B−C=A+B+C−B
7 5 6 syld3an1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B-B−C=A+B+C−B
8 pnncan ⊢B∈ℂ∧A∈ℂ∧C∈ℂ→B+A-B−C=A+C
9 8 3com12 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+A-B−C=A+C
10 3 7 9 3eqtr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B+C−B=A+C