Metamath Proof Explorer


Axiom ax-mulass

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

Ref Expression
Assertion ax-mulass A B C A B C = A B C

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 cC class C
6 5 1 wcel wff C
7 2 4 6 w3a wff A B C
8 cmul class ×
9 0 3 8 co class A B
10 9 5 8 co class A B C
11 3 5 8 co class B C
12 0 11 8 co class A B C
13 10 12 wceq wff A B C = A B C
14 7 13 wi wff A B C A B C = A B C