Metamath Proof Explorer


Axiom ax-mulcom

Description: Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, justified by Theorem axmulcom . Proofs should normally use mulcom instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

Ref Expression
Assertion ax-mulcom A B A B = B A

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cc class
2 0 1 wcel wff A
3 cB class B
4 3 1 wcel wff B
5 2 4 wa wff A B
6 cmul class ×
7 0 3 6 co class A B
8 3 0 6 co class B A
9 7 8 wceq wff A B = B A
10 5 9 wi wff A B A B = B A