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