Metamath Proof Explorer

Theorem sub32

Description: Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005)

Ref Expression
Assertion sub32 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - B - C = A - C - B

Proof

Step Hyp Ref Expression
1 addcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
2 1 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
3 2 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + C = A − C + B
4 subsub4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - B - C = A − B + C
5 subsub4 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A - C - B = A − C + B
6 5 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - C - B = A − C + B
7 3 4 6 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - B - C = A - C - B