Theorem mulcomd 7445

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 7407	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	syl2anc 403	1 ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Syntax hints:   → wi 4   = wceq 1287   ∈ wcel 1436  (class class class)co 5606  ℂcc 7284   · cmul 7291

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

This theorem is referenced by:  mul31  7549  remulext2  8010  mulreim  8014  mulext2  8023  mulcanapd  8061  mulcanap2d  8062  divcanap1  8079  divrecap2  8087  div23ap  8089  divdivdivap  8111  divmuleqap  8115  divadddivap  8125  divcanap5rd  8214  dmdcanap2d  8217  mvllmulapd  8231  prodgt0  8240  lt2mul2div  8267  mulle0r  8332  qapne  9048  modqvalr  9652  modqcyc  9686  mulp1mod1  9692  modqmul12d  9705  modqnegd  9706  modqmulmodr  9717  addmodlteq  9725  expaddzap  9889  binom2  9954  binom3  9959  bccmpl  10050  bcm1k  10056  bcn2  10060  bcpasc  10062  cvg1nlemcxze  10302  cvg1nlemcau  10304  resqrexlemcalc1  10334  resqrexlemcalc2  10335  resqrexlemnm  10338  recvalap  10417  nndivides  10669  dvds2ln  10695  even2n  10740  oddm1even  10741  m1exp1  10767  divalgmod  10793  mulgcdr  10873  rplpwr  10882  lcmgcdlem  10925  divgcdcoprmex  10950  cncongr1  10951  oddpwdclemxy  11013  2sqpwodd  11020  evenennn  11072