Metamath Proof Explorer

Theorem sub4

Description: Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007)

Ref Expression
Assertion sub4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A - B - C − D = A - C - B − D

Proof

Step Hyp Ref Expression
1 addcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
2 1 ad2ant2lr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B + C = C + B
3 2 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + D - B + C = A + D - C + B
4 subadd4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A - B - C − D = A + D - B + C
5 subadd4 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A - C - B − D = A + D - C + B
6 5 an4s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A - C - B − D = A + D - C + B
7 3 4 6 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A - B - C − D = A - C - B − D