Theorem mulcomd 8353

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 8314	. 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 8183   · cmul 8190

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

This theorem is used by:  mul31  8464  remulext2  8936  mulreim  8940  mulext2  8949  mulcanapd  8997  mulcanap2d  8998  divcanap1  9019  divrecap2  9027  div23ap  9029  divdivdivap  9051  divmuleqap  9055  divadddivap  9065  apmul2  9127  apdivmuld  9151  divcanap5rd  9156  dmdcanap2d  9159  mvllmulapd  9180  prodgt0  9190  lt2mul2div  9217  mulle0r  9282  subhalfhalf  9551  qapne  10054  irrmulap  10064  mul2lt0llt0  10178  mul2lt0lgt0  10179  mul2lt0pn  10181  modqvalr  10782  modqcyc  10816  mulp1mod1  10822  modqmul12d  10835  modqnegd  10836  modqmulmodr  10847  addmodlteq  10855  expaddzap  11040  binom2  11108  binom3  11114  bccmpl  11213  bcm1k  11219  bcn2  11223  bcpasc  11225  cvg1nlemcxze  11769  cvg1nlemcau  11771  resqrexlemcalc1  11801  resqrexlemcalc2  11802  resqrexlemnm  11805  recvalap  11885  bdtrilem  12029  reccn2ap  12103  isummulc1  12218  fsummulc1  12240  trireciplem  12291  geolim  12302  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemfm  12320  cvgratz  12323  mertensabs  12328  eftlub  12481  sinadd  12527  cosadd  12528  sin2t  12540  nndivides  12588  dvds2ln  12615  even2n  12665  oddm1even  12666  m1exp1  12692  divalgmod  12718  bitsp1  12742  bitsinv1lem  12752  mulgcdr  12819  rplpwr  12828  lcmgcdlem  12879  divgcdcoprmex  12904  cncongr1  12905  nnmaxpwlemxy  12972  2sqpwodd  12980  eulerthlema  13036  eulerthlemth  13038  prmdiv  13041  prmdivdiv  13043  modprmn0modprm0  13063  coprimeprodsq  13064  pythagtriplem6  13077  pythagtriplem7  13078  pceulem  13101  pcadd  13147  prmpwdvds  13162  mul4sqlem  13200  4sqlem17  13214  evenennn  13341  mulgassr  14021  znunit  15102  dvmulxxbr  15945  dvmptcmulcn  15964  dvply1  16008  tangtx  16082  logdivlt  16141  cxpmul  16162  abscxp  16167  efnthr  16193  binom4  16236  pellexlem2  16247  wilthlem1  16249  mpodvdsmulf1o  16301  sgmppw  16303  perfect1  16315  lgsdirprm  16375  lgsdi  16378  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1a  16399  gausslemma2dlem6  16408  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2  16424  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  2lgsoddprmlem2  16447  2sqlem3  16458  2sqlem4  16459  dichmul0orlem3  16977