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

Metamath Proof Explorer

Theorem add4

Description: Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion add4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C + D = A + C + B + D

Proof

Step Hyp Ref Expression
1 add12 ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B + C + D = C + B + D
2 1 3expb ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B + C + D = C + B + D
3 2 oveq2d ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C + D = A + C + B + D
4 3 adantll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C + D = A + C + B + D
5 addcl ⊢ C ∈ ℂ ∧ D ∈ ℂ → C + D ∈ ℂ
6 addass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C + D ∈ ℂ → A + B + C + D = A + B + C + D
7 6 3expa ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C + D ∈ ℂ → A + B + C + D = A + B + C + D
8 5 7 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C + D = A + B + C + D
9 addcl ⊢ B ∈ ℂ ∧ D ∈ ℂ → B + D ∈ ℂ
10 addass ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B + D ∈ ℂ → A + C + B + D = A + C + B + D
11 10 3expa ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B + D ∈ ℂ → A + C + B + D = A + C + B + D
12 9 11 sylan2 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A + C + B + D = A + C + B + D
13 12 an4s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + C + B + D = A + C + B + D
14 4 8 13 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C + D = A + C + B + D