Metamath Proof Explorer

Theorem sub31

Description: Swap the first and third terms in a double subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion sub31 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = C − B − A

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
2 simpr ⊢ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
3 simpl ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
4 2 3 subcld ⊢ B ∈ ℂ ∧ C ∈ ℂ → C − B ∈ ℂ
5 4 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C − B ∈ ℂ
6 1 5 addcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C - B = C - B + A
7 subsub2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = A + C - B
8 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
9 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
10 8 9 1 subsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C − B − A = C - B + A
11 6 7 10 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B − C = C − B − A