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