Theorem mulcomd 8201

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   · cmul 8037

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

This theorem is referenced by:  mul31  8310  remulext2  8780  mulreim  8784  mulext2  8793  mulcanapd  8841  mulcanap2d  8842  divcanap1  8861  divrecap2  8869  div23ap  8871  divdivdivap  8893  divmuleqap  8897  divadddivap  8907  apmul2  8969  apdivmuld  8993  divcanap5rd  8998  dmdcanap2d  9001  mvllmulapd  9022  prodgt0  9032  lt2mul2div  9059  mulle0r  9124  subhalfhalf  9379  qapne  9873  irrmulap  9882  mul2lt0llt0  9996  mul2lt0lgt0  9997  mul2lt0pn  9999  modqvalr  10588  modqcyc  10622  mulp1mod1  10628  modqmul12d  10641  modqnegd  10642  modqmulmodr  10653  addmodlteq  10661  expaddzap  10846  binom2  10914  binom3  10920  bccmpl  11017  bcm1k  11023  bcn2  11027  bcpasc  11029  cvg1nlemcxze  11544  cvg1nlemcau  11546  resqrexlemcalc1  11576  resqrexlemcalc2  11577  resqrexlemnm  11580  recvalap  11659  bdtrilem  11801  reccn2ap  11875  isummulc1  11990  fsummulc1  12012  trireciplem  12063  geolim  12074  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  cvgratnnlemfm  12092  cvgratz  12095  mertensabs  12100  eftlub  12253  sinadd  12299  cosadd  12300  sin2t  12312  nndivides  12360  dvds2ln  12387  even2n  12437  oddm1even  12438  m1exp1  12464  divalgmod  12490  bitsp1  12514  bitsinv1lem  12524  mulgcdr  12591  rplpwr  12600  lcmgcdlem  12651  divgcdcoprmex  12676  cncongr1  12677  oddpwdclemxy  12743  2sqpwodd  12750  eulerthlema  12804  eulerthlemth  12806  prmdiv  12809  prmdivdiv  12811  modprmn0modprm0  12831  coprimeprodsq  12832  pythagtriplem6  12845  pythagtriplem7  12846  pceulem  12869  pcadd  12915  prmpwdvds  12930  mul4sqlem  12968  4sqlem17  12982  evenennn  13016  mulgassr  13749  znunit  14676  dvmulxxbr  15429  dvmptcmulcn  15448  dvply1  15492  tangtx  15565  cxpmul  15639  abscxp  15642  binom4  15706  wilthlem1  15707  mpodvdsmulf1o  15717  sgmppw  15719  perfect1  15725  lgsdirprm  15766  lgsdi  15769  lgsdirnn0  15779  lgsdinn0  15780  gausslemma2dlem1a  15790  gausslemma2dlem6  15799  lgsquadlem1  15809  lgsquadlem2  15810  lgsquadlem3  15811  lgsquad2  15815  2lgslem3a1  15829  2lgslem3b1  15830  2lgslem3c1  15831  2lgslem3d1  15832  2lgsoddprmlem2  15838  2sqlem3  15849  2sqlem4  15850