Metamath Proof Explorer


Theorem add12i

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

Ref Expression
Hypotheses add.1 𝐴 ∈ ℂ
add.2 𝐵 ∈ ℂ
add.3 𝐶 ∈ ℂ
Assertion add12i ( 𝐴 + ( 𝐵 + 𝐶 ) ) = ( 𝐵 + ( 𝐴 + 𝐶 ) )

Proof

Step Hyp Ref Expression
1 add.1 𝐴 ∈ ℂ
2 add.2 𝐵 ∈ ℂ
3 add.3 𝐶 ∈ ℂ
4 add12 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + ( 𝐵 + 𝐶 ) ) = ( 𝐵 + ( 𝐴 + 𝐶 ) ) )
5 1 2 3 4 mp3an ( 𝐴 + ( 𝐵 + 𝐶 ) ) = ( 𝐵 + ( 𝐴 + 𝐶 ) )