Metamath Proof Explorer

Theorem subadd4

Description: Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006)

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

Proof

Step Hyp Ref Expression
1 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
2 subsub2 ⊢ A − B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A - B - C − D = A − B + D - C
3 2 3expb ⊢ A − B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A - B - C − D = A − B + D - C
4 1 3 sylan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A - B - C − D = A − B + D - C
5 addsub4 ⊢ A ∈ ℂ ∧ D ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + D - B + C = A − B + D - C
6 5 an42s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + D - B + C = A − B + D - C
7 4 6 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A - B - C − D = A + D - B + C