# Metamath Proof Explorer

## Theorem pnncan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005) (Revised by Mario Carneiro, 27-May-2016)

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

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}\in ℂ$
2 simp2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}\in ℂ$
3 1 2 addcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}\in ℂ$
4 simp3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {C}\in ℂ$
5 subsub ${⊢}\left({A}+{B}\in ℂ\wedge {A}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-\left({A}-{C}\right)=\left({A}+{B}\right)-{A}+{C}$
6 3 1 4 5 syl3anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-\left({A}-{C}\right)=\left({A}+{B}\right)-{A}+{C}$
7 pncan2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}-{A}={B}$
8 7 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-{A}={B}$
9 8 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}+{B}\right)-{A}+{C}={B}+{C}$
10 6 9 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-\left({A}-{C}\right)={B}+{C}$