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

Metamath Proof Explorer

Theorem addcomi

Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 mul.1 ⊢ 𝐴 ∈ ℂ
2 mul.2 ⊢ 𝐵 ∈ ℂ
3 addcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
4 1 2 3 mp2an ⊢ ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 )