Metamath Proof Explorer

Theorem add12

Description: Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 11-May-2004)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
2 1 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + C = B + A + C
3 2 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = B + A + C
4 addass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = A + B + C
5 addass ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ → B + A + C = B + A + C
6 5 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + A + C = B + A + C
7 3 4 6 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C = B + A + C