This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addcomli

Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Hypotheses mul.1 ⊢ 𝐴 ∈ ℂ
mul.2 ⊢ 𝐵 ∈ ℂ
addcomli.2 ⊢ ( 𝐴 + 𝐵 ) = 𝐶
Assertion addcomli ( 𝐵 + 𝐴 ) = 𝐶

Proof

Step Hyp Ref Expression
1 mul.1 ⊢ 𝐴 ∈ ℂ
2 mul.2 ⊢ 𝐵 ∈ ℂ
3 addcomli.2 ⊢ ( 𝐴 + 𝐵 ) = 𝐶
4 2 1 addcomi ⊢ ( 𝐵 + 𝐴 ) = ( 𝐴 + 𝐵 )
5 4 3 eqtri ⊢ ( 𝐵 + 𝐴 ) = 𝐶