Metamath Proof Explorer

Theorem subsub

Description: Law for double subtraction. (Contributed by NM, 13-May-2004)

Ref Expression
Assertion subsub ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = A - B + C

Proof

Step Hyp Ref Expression
1 subsub2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = A + C - B
2 addsubass ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A + C - B = A + C - B
3 addsub ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A + C - B = A - B + C
4 2 3 eqtr3d ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A + C - B = A - B + C
5 4 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C - B = A - B + C
6 1 5 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = A - B + C