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

Metamath Proof Explorer

Theorem addsub4

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

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

Proof

Step Hyp Ref Expression
1 simpll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ∈ ℂ
2 simplr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B ∈ ℂ
3 simprl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → C ∈ ℂ
4 addsub ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - C = A - C + B
5 1 2 3 4 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B - C = A - C + B
6 5 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B - C - D = A − C + B - D
7 1 2 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ∈ ℂ
8 simprr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → D ∈ ℂ
9 subsub4 ⊢ A + B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B - C - D = A + B - C + D
10 7 3 8 9 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B - C - D = A + B - C + D
11 subcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A − C ∈ ℂ
12 11 ad2ant2r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A − C ∈ ℂ
13 addsubass ⊢ A − C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A − C + B - D = A − C + B - D
14 12 2 8 13 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A − C + B - D = A − C + B - D
15 6 10 14 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B - C + D = A − C + B - D