Metamath Proof Explorer

Theorem add32

Description: Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 13-Nov-1999)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
2 1 oveq2d ⊢ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + C + B
3 2 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + C + B
4 addass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + B + C
5 addass ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A + C + B = A + C + B
6 5 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C + B = A + C + B
7 3 4 6 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + C + B