# Metamath Proof Explorer

## Theorem subsub2

Description: Law for double subtraction. (Contributed by NM, 30-Jun-2005) (Revised by Mario Carneiro, 27-May-2016)

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

### Proof

Step Hyp Ref Expression
1 subcl ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}\in ℂ$
2 1 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}\in ℂ$
3 simp1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}\in ℂ$
4 simp3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {C}\in ℂ$
5 simp2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}\in ℂ$
6 subcl ${⊢}\left({C}\in ℂ\wedge {B}\in ℂ\right)\to {C}-{B}\in ℂ$
7 4 5 6 syl2anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {C}-{B}\in ℂ$
8 2 3 7 add12d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({B}-{C}\right)+{A}+\left({C}-{B}\right)={A}+\left({B}-{C}\right)+\left({C}-{B}\right)$
9 npncan2 ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to \left({B}-{C}\right)+{C}-{B}=0$
10 9 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({B}-{C}\right)+{C}-{B}=0$
11 10 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+\left({B}-{C}\right)+\left({C}-{B}\right)={A}+0$
12 3 addid1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+0={A}$
13 8 11 12 3eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({B}-{C}\right)+{A}+\left({C}-{B}\right)={A}$
14 3 7 addcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{C}-{B}\in ℂ$
15 subadd ${⊢}\left({A}\in ℂ\wedge {B}-{C}\in ℂ\wedge {A}+{C}-{B}\in ℂ\right)\to \left({A}-\left({B}-{C}\right)={A}+{C}-{B}↔\left({B}-{C}\right)+{A}+\left({C}-{B}\right)={A}\right)$
16 3 2 14 15 syl3anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-\left({B}-{C}\right)={A}+{C}-{B}↔\left({B}-{C}\right)+{A}+\left({C}-{B}\right)={A}\right)$
17 13 16 mpbird ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}-\left({B}-{C}\right)={A}+{C}-{B}$