Axiom ax-mulcom 11171

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

Assertion

Ref	Expression
ax-mulcom	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Detailed syntax breakdown of Axiom ax-mulcom

Step	Hyp	Ref	Expression
1		cA	. . . 4 class 𝐴
2		cc 11105	. . . 4 class ℂ
3	1, 2	wcel 2107	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2107	. . 3 wff 𝐵 ∈ ℂ
6	3, 5	wa 397	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)
7		cmul 11112	. . . 4 class ·
8	1, 4, 7	co 7406	. . 3 class (𝐴 · 𝐵)
9	4, 1, 7	co 7406	. . 3 class (𝐵 · 𝐴)
10	8, 9	wceq 1542	. 2 wff (𝐴 · 𝐵) = (𝐵 · 𝐴)
11	6, 10	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

This axiom is referenced by:  mulcom  11193