Metamath Proof Explorer

Theorem add32r

Description: Commutative/associative law that swaps the last two terms in a triple sum, rearranging the parentheses. (Contributed by Paul Chapman, 18-May-2007)

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

Proof

Step Hyp Ref Expression
1 addass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + B + C
2 add32 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + C + B
3 1 2 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + C + B