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