This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℂ \land B \in ℂ) \to A B = B A$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cc	$class ℂ$
2	0 1	wcel	$wff A \in ℂ$
3		cB	$class B$
4	3 1	wcel	$wff B \in ℂ$
5	2 4	wa	$wff (A \in ℂ \land B \in ℂ)$
6		cmul	$class \times$
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 \in ℂ \land B \in ℂ) \to A B = B A)$