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

Metamath Proof Explorer

Theorem subadd4b

Description: Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses subadd4b.1 ⊢ φ → A ∈ ℂ
subadd4b.2 ⊢ φ → B ∈ ℂ
subadd4b.3 ⊢ φ → C ∈ ℂ
subadd4b.4 ⊢ φ → D ∈ ℂ
Assertion subadd4b ⊢ φ → A − B + C - D = A − D + C - B

Proof

Step Hyp Ref Expression
1 subadd4b.1 ⊢ φ → A ∈ ℂ
2 subadd4b.2 ⊢ φ → B ∈ ℂ
3 subadd4b.3 ⊢ φ → C ∈ ℂ
4 subadd4b.4 ⊢ φ → D ∈ ℂ
5 1 2 4 3 subadd4d ⊢ φ → A - B - D − C = A + C - B + D
6 1 2 subcld ⊢ φ → A − B ∈ ℂ
7 6 4 3 subsub2d ⊢ φ → A - B - D − C = A − B + C - D
8 2 4 addcomd ⊢ φ → B + D = D + B
9 8 oveq2d ⊢ φ → A + C - B + D = A + C - D + B
10 1 3 4 2 addsub4d ⊢ φ → A + C - D + B = A − D + C - B
11 9 10 eqtrd ⊢ φ → A + C - B + D = A − D + C - B
12 5 7 11 3eqtr3d ⊢ φ → A − B + C - D = A − D + C - B