Theorem mulcomd 8348

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8178   · cmul 8185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcom 8281

This theorem is used by:  mul31  8459  remulext2  8931  mulreim  8935  mulext2  8944  mulcanapd  8992  mulcanap2d  8993  divcanap1  9014  divrecap2  9022  div23ap  9024  divdivdivap  9046  divmuleqap  9050  divadddivap  9060  apmul2  9122  apdivmuld  9146  divcanap5rd  9151  dmdcanap2d  9154  mvllmulapd  9175  prodgt0  9185  lt2mul2div  9212  mulle0r  9277  subhalfhalf  9545  qapne  10049  irrmulap  10059  mul2lt0llt0  10173  mul2lt0lgt0  10174  mul2lt0pn  10176  modqvalr  10777  modqcyc  10811  mulp1mod1  10817  modqmul12d  10830  modqnegd  10831  modqmulmodr  10842  addmodlteq  10850  expaddzap  11035  binom2  11103  binom3  11109  bccmpl  11208  bcm1k  11214  bcn2  11218  bcpasc  11220  cvg1nlemcxze  11764  cvg1nlemcau  11766  resqrexlemcalc1  11796  resqrexlemcalc2  11797  resqrexlemnm  11800  recvalap  11880  bdtrilem  12024  reccn2ap  12098  isummulc1  12213  fsummulc1  12235  trireciplem  12286  geolim  12297  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemfm  12315  cvgratz  12318  mertensabs  12323  eftlub  12476  sinadd  12522  cosadd  12523  sin2t  12535  nndivides  12583  dvds2ln  12610  even2n  12660  oddm1even  12661  m1exp1  12687  divalgmod  12713  bitsp1  12737  bitsinv1lem  12747  mulgcdr  12814  rplpwr  12823  lcmgcdlem  12874  divgcdcoprmex  12899  cncongr1  12900  nnmaxpwlemxy  12967  2sqpwodd  12975  eulerthlema  13031  eulerthlemth  13033  prmdiv  13036  prmdivdiv  13038  modprmn0modprm0  13058  coprimeprodsq  13059  pythagtriplem6  13072  pythagtriplem7  13073  pceulem  13096  pcadd  13142  prmpwdvds  13157  mul4sqlem  13195  4sqlem17  13209  evenennn  13336  mulgassr  14016  znunit  15078  dvmulxxbr  15894  dvmptcmulcn  15913  dvply1  15957  tangtx  16031  logdivlt  16090  cxpmul  16111  abscxp  16116  efnthr  16142  binom4  16185  pellexlem2  16196  wilthlem1  16198  mpodvdsmulf1o  16250  sgmppw  16252  perfect1  16264  lgsdirprm  16324  lgsdi  16327  lgsdirnn0  16337  lgsdinn0  16338  gausslemma2dlem1a  16348  gausslemma2dlem6  16357  lgsquadlem1  16367  lgsquadlem2  16368  lgsquadlem3  16369  lgsquad2  16373  2lgslem3a1  16387  2lgslem3b1  16388  2lgslem3c1  16389  2lgslem3d1  16390  2lgsoddprmlem2  16396  2sqlem3  16407  2sqlem4  16408  dichmul0orlem3  16926