This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subsub3

Description: Law for double subtraction. (Contributed by NM, 27-Jul-2005)

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

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 2 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C - B = A + C - B
4 1 3 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = A + C - B