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 ⊢ A ∈ ℂ
axi.2 ⊢ B ∈ ℂ
mulcomli.3 ⊢ A ⁢ B = C
Assertion mulcomli ⊢ B ⁢ A = C

Proof

Step Hyp Ref Expression
1 axi.1 ⊢ A ∈ ℂ
2 axi.2 ⊢ B ∈ ℂ
3 mulcomli.3 ⊢ A ⁢ B = C
4 2 1 mulcomi ⊢ B ⁢ A = A ⁢ B
5 4 3 eqtri ⊢ B ⁢ A = C