Metamath Proof Explorer

Theorem add42

Description: Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005)

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

Proof

Step Hyp Ref Expression
1 add4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C + D = A + C + B + D
2 addcom ⊢ B ∈ ℂ ∧ D ∈ ℂ → B + D = D + B
3 2 ad2ant2l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B + D = D + B
4 3 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + C + B + D = A + C + D + B
5 1 4 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + C + D = A + C + D + B