Theorem mulcomd 8354

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

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

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

This theorem is used by:  mul31  8465  remulext2  8937  mulreim  8941  mulext2  8950  mulcanapd  8998  mulcanap2d  8999  divcanap1  9020  divrecap2  9028  div23ap  9030  divdivdivap  9052  divmuleqap  9056  divadddivap  9066  apmul2  9128  apdivmuld  9152  divcanap5rd  9157  dmdcanap2d  9160  mvllmulapd  9181  prodgt0  9191  lt2mul2div  9218  mulle0r  9283  subhalfhalf  9552  qapne  10056  irrmulap  10066  mul2lt0llt0  10180  mul2lt0lgt0  10181  mul2lt0pn  10183  modqvalr  10784  modqcyc  10818  mulp1mod1  10824  modqmul12d  10837  modqnegd  10838  modqmulmodr  10849  addmodlteq  10857  expaddzap  11042  binom2  11110  binom3  11116  bccmpl  11215  bcm1k  11221  bcn2  11225  bcpasc  11227  cvg1nlemcxze  11771  cvg1nlemcau  11773  resqrexlemcalc1  11803  resqrexlemcalc2  11804  resqrexlemnm  11807  recvalap  11887  bdtrilem  12031  reccn2ap  12105  isummulc1  12220  fsummulc1  12242  trireciplem  12293  geolim  12304  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  cvgratnnlemfm  12322  cvgratz  12325  mertensabs  12330  eftlub  12483  sinadd  12529  cosadd  12530  sin2t  12542  nndivides  12590  dvds2ln  12617  even2n  12667  oddm1even  12668  m1exp1  12694  divalgmod  12720  bitsp1  12744  bitsinv1lem  12754  mulgcdr  12821  rplpwr  12830  lcmgcdlem  12881  divgcdcoprmex  12906  cncongr1  12907  nnmaxpwlemxy  12974  2sqpwodd  12982  eulerthlema  13038  eulerthlemth  13040  prmdiv  13043  prmdivdiv  13045  modprmn0modprm0  13065  coprimeprodsq  13066  pythagtriplem6  13079  pythagtriplem7  13080  pceulem  13103  pcadd  13149  prmpwdvds  13164  mul4sqlem  13202  4sqlem17  13216  evenennn  13343  mulgassr  14023  znunit  15104  dvmulxxbr  15940  dvmptcmulcn  15959  dvply1  16003  tangtx  16077  logdivlt  16136  cxpmul  16157  abscxp  16162  efnthr  16188  binom4  16231  pellexlem2  16242  wilthlem1  16244  mpodvdsmulf1o  16296  sgmppw  16298  perfect1  16310  lgsdirprm  16370  lgsdi  16373  lgsdirnn0  16383  lgsdinn0  16384  gausslemma2dlem1a  16394  gausslemma2dlem6  16403  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  lgsquad2  16419  2lgslem3a1  16433  2lgslem3b1  16434  2lgslem3c1  16435  2lgslem3d1  16436  2lgsoddprmlem2  16442  2sqlem3  16453  2sqlem4  16454  dichmul0orlem3  16972