# Metamath Proof Explorer

## Theorem npncan

Description: Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005)

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

### Proof

Step Hyp Ref Expression
1 subcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}-{B}\in ℂ$
2 1 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}-{B}\in ℂ$
3 addsubass ${⊢}\left({A}-{B}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{B}\right)+{B}-{C}=\left({A}-{B}\right)+{B}-{C}$
4 2 3 syld3an1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{B}\right)+{B}-{C}=\left({A}-{B}\right)+{B}-{C}$
5 npcan ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}-{B}+{B}={A}$
6 5 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left({A}-{B}\right)+{B}-{C}={A}-{C}$
7 6 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{B}\right)+{B}-{C}={A}-{C}$
8 4 7 eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{B}\right)+{B}-{C}={A}-{C}$