MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-mulass Unicode version

Axiom ax-mulass 9579
Description: Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by theorem axmulass 9555. Proofs should normally use mulass 9601 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
ax-mulass

Detailed syntax breakdown of Axiom ax-mulass
StepHypRef Expression
1 cA . . . 4
2 cc 9511 . . . 4
31, 2wcel 1818 . . 3
4 cB . . . 4
54, 2wcel 1818 . . 3
6 cC . . . 4
76, 2wcel 1818 . . 3
83, 5, 7w3a 973 . 2
9 cmul 9518 . . . . 5
101, 4, 9co 6296 . . . 4
1110, 6, 9co 6296 . . 3
124, 6, 9co 6296 . . . 4
131, 12, 9co 6296 . . 3
1411, 13wceq 1395 . 2
158, 14wi 4 1
Colors of variables: wff setvar class
This axiom is referenced by:  mulass  9601
  Copyright terms: Public domain W3C validator