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

Metamath Proof Explorer

Theorem mulcomli

Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994)

Ref Expression
Hypotheses axi.1 ⊢ 𝐴 ∈ ℂ
axi.2 ⊢ 𝐵 ∈ ℂ
mulcomli.3 ⊢ ( 𝐴 · 𝐵 ) = 𝐶
Assertion mulcomli ( 𝐵 · 𝐴 ) = 𝐶

Proof

Step Hyp Ref Expression
1 axi.1 ⊢ 𝐴 ∈ ℂ
2 axi.2 ⊢ 𝐵 ∈ ℂ
3 mulcomli.3 ⊢ ( 𝐴 · 𝐵 ) = 𝐶
4 2 1 mulcomi ⊢ ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 )
5 4 3 eqtri ⊢ ( 𝐵 · 𝐴 ) = 𝐶