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 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = A + C - B

Proof

Step Hyp Ref Expression
1 subcl ⊢ B ∈ ℂ ∧ C ∈ ℂ → B − C ∈ ℂ
2 1 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B − C ∈ ℂ
3 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
4 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
5 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
6 subcl ⊢ C ∈ ℂ ∧ B ∈ ℂ → C − B ∈ ℂ
7 4 5 6 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C − B ∈ ℂ
8 2 3 7 add12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B − C + A + C − B = A + B − C + C − B
9 npncan2 ⊢ B ∈ ℂ ∧ C ∈ ℂ → B − C + C - B = 0
10 9 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B − C + C - B = 0
11 10 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B − C + C − B = A + 0
12 3 addridd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + 0 = A
13 8 11 12 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B − C + A + C − B = A
14 3 7 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C - B ∈ ℂ
15 subadd ⊢ A ∈ ℂ ∧ B − C ∈ ℂ ∧ A + C - B ∈ ℂ → A − B − C = A + C - B ↔ B − C + A + C − B = A
16 3 2 14 15 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = A + C - B ↔ B − C + A + C − B = A
17 13 16 mpbird ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = A + C - B