Theorem mulcomd 8291

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121   · cmul 8128

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

This theorem is referenced by:  mul31  8400  remulext2  8870  mulreim  8874  mulext2  8883  mulcanapd  8931  mulcanap2d  8932  divcanap1  8951  divrecap2  8959  div23ap  8961  divdivdivap  8983  divmuleqap  8987  divadddivap  8997  apmul2  9059  apdivmuld  9083  divcanap5rd  9088  dmdcanap2d  9091  mvllmulapd  9112  prodgt0  9122  lt2mul2div  9149  mulle0r  9214  subhalfhalf  9469  qapne  9967  irrmulap  9976  mul2lt0llt0  10090  mul2lt0lgt0  10091  mul2lt0pn  10093  modqvalr  10683  modqcyc  10717  mulp1mod1  10723  modqmul12d  10736  modqnegd  10737  modqmulmodr  10748  addmodlteq  10756  expaddzap  10941  binom2  11009  binom3  11015  bccmpl  11112  bcm1k  11118  bcn2  11122  bcpasc  11124  cvg1nlemcxze  11660  cvg1nlemcau  11662  resqrexlemcalc1  11692  resqrexlemcalc2  11693  resqrexlemnm  11696  recvalap  11775  bdtrilem  11917  reccn2ap  11991  isummulc1  12106  fsummulc1  12128  trireciplem  12179  geolim  12190  cvgratnnlemnexp  12203  cvgratnnlemmn  12204  cvgratnnlemfm  12208  cvgratz  12211  mertensabs  12216  eftlub  12369  sinadd  12415  cosadd  12416  sin2t  12428  nndivides  12476  dvds2ln  12503  even2n  12553  oddm1even  12554  m1exp1  12580  divalgmod  12606  bitsp1  12630  bitsinv1lem  12640  mulgcdr  12707  rplpwr  12716  lcmgcdlem  12767  divgcdcoprmex  12792  cncongr1  12793  oddpwdclemxy  12859  2sqpwodd  12866  eulerthlema  12920  eulerthlemth  12922  prmdiv  12925  prmdivdiv  12927  modprmn0modprm0  12947  coprimeprodsq  12948  pythagtriplem6  12961  pythagtriplem7  12962  pceulem  12985  pcadd  13031  prmpwdvds  13046  mul4sqlem  13084  4sqlem17  13098  evenennn  13133  mulgassr  13866  znunit  14794  dvmulxxbr  15554  dvmptcmulcn  15573  dvply1  15617  tangtx  15690  cxpmul  15764  abscxp  15767  binom4  15831  pellexlem2  15833  wilthlem1  15835  mpodvdsmulf1o  15845  sgmppw  15847  perfect1  15853  lgsdirprm  15894  lgsdi  15897  lgsdirnn0  15907  lgsdinn0  15908  gausslemma2dlem1a  15918  gausslemma2dlem6  15927  lgsquadlem1  15937  lgsquadlem2  15938  lgsquadlem3  15939  lgsquad2  15943  2lgslem3a1  15957  2lgslem3b1  15958  2lgslem3c1  15959  2lgslem3d1  15960  2lgsoddprmlem2  15966  2sqlem3  15977  2sqlem4  15978