# Metamath Proof Explorer

## Theorem ppncan

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

Ref Expression
Assertion ppncan ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}+\left({C}-{B}\right)={A}+{C}$

### Proof

Step Hyp Ref Expression
1 addcom ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}={B}+{A}$
2 1 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}={B}+{A}$
3 2 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-\left({B}-{C}\right)={B}+{A}-\left({B}-{C}\right)$
4 addcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}\in ℂ$
5 4 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}\in ℂ$
6 subsub2 ${⊢}\left({A}+{B}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-\left({B}-{C}\right)={A}+{B}+\left({C}-{B}\right)$
7 5 6 syld3an1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-\left({B}-{C}\right)={A}+{B}+\left({C}-{B}\right)$
8 pnncan ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\wedge {C}\in ℂ\right)\to {B}+{A}-\left({B}-{C}\right)={A}+{C}$
9 8 3com12 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}+{A}-\left({B}-{C}\right)={A}+{C}$
10 3 7 9 3eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}+\left({C}-{B}\right)={A}+{C}$