Theorem mulcomd 8206

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035   · cmul 8042

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

This theorem is referenced by:  mul31  8315  remulext2  8785  mulreim  8789  mulext2  8798  mulcanapd  8846  mulcanap2d  8847  divcanap1  8866  divrecap2  8874  div23ap  8876  divdivdivap  8898  divmuleqap  8902  divadddivap  8912  apmul2  8974  apdivmuld  8998  divcanap5rd  9003  dmdcanap2d  9006  mvllmulapd  9027  prodgt0  9037  lt2mul2div  9064  mulle0r  9129  subhalfhalf  9384  qapne  9878  irrmulap  9887  mul2lt0llt0  10001  mul2lt0lgt0  10002  mul2lt0pn  10004  modqvalr  10593  modqcyc  10627  mulp1mod1  10633  modqmul12d  10646  modqnegd  10647  modqmulmodr  10658  addmodlteq  10666  expaddzap  10851  binom2  10919  binom3  10925  bccmpl  11022  bcm1k  11028  bcn2  11032  bcpasc  11034  cvg1nlemcxze  11565  cvg1nlemcau  11567  resqrexlemcalc1  11597  resqrexlemcalc2  11598  resqrexlemnm  11601  recvalap  11680  bdtrilem  11822  reccn2ap  11896  isummulc1  12011  fsummulc1  12033  trireciplem  12084  geolim  12095  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  cvgratnnlemfm  12113  cvgratz  12116  mertensabs  12121  eftlub  12274  sinadd  12320  cosadd  12321  sin2t  12333  nndivides  12381  dvds2ln  12408  even2n  12458  oddm1even  12459  m1exp1  12485  divalgmod  12511  bitsp1  12535  bitsinv1lem  12545  mulgcdr  12612  rplpwr  12621  lcmgcdlem  12672  divgcdcoprmex  12697  cncongr1  12698  oddpwdclemxy  12764  2sqpwodd  12771  eulerthlema  12825  eulerthlemth  12827  prmdiv  12830  prmdivdiv  12832  modprmn0modprm0  12852  coprimeprodsq  12853  pythagtriplem6  12866  pythagtriplem7  12867  pceulem  12890  pcadd  12936  prmpwdvds  12951  mul4sqlem  12989  4sqlem17  13003  evenennn  13037  mulgassr  13770  znunit  14697  dvmulxxbr  15455  dvmptcmulcn  15474  dvply1  15518  tangtx  15591  cxpmul  15665  abscxp  15668  binom4  15732  wilthlem1  15733  mpodvdsmulf1o  15743  sgmppw  15745  perfect1  15751  lgsdirprm  15792  lgsdi  15795  lgsdirnn0  15805  lgsdinn0  15806  gausslemma2dlem1a  15816  gausslemma2dlem6  15825  lgsquadlem1  15835  lgsquadlem2  15836  lgsquadlem3  15837  lgsquad2  15841  2lgslem3a1  15855  2lgslem3b1  15856  2lgslem3c1  15857  2lgslem3d1  15858  2lgsoddprmlem2  15864  2sqlem3  15875  2sqlem4  15876