Theorem mulcomd 7048

Description: Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
mulcomd	⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Proof of Theorem mulcomd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		mulcom 7010	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	syl2anc 391	1 ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Syntax hints:   → wi 4   = wceq 1243   ∈ wcel 1393  (class class class)co 5512  ℂcc 6887   · cmul 6894

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulcom 6985

This theorem is referenced by:  mul31  7144  remulext2  7591  mulreim  7595  mulext2  7604  mulcanapd  7642  mulcanap2d  7643  divcanap1  7660  divrecap2  7668  div23ap  7670  divdivdivap  7689  divmuleqap  7693  divadddivap  7703  divcanap5rd  7792  dmdcanap2d  7795  mvllmulapd  7809  prodgt0  7818  lt2mul2div  7845  qapne  8574  modqvalr  9167  expaddzap  9299  binom2  9362  binom3  9366  cvg1nlemcxze  9581  cvg1nlemcau  9583  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemnm  9616  recvalap  9693