Theorem mulcomd 8347

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 8308	. 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 8177   · cmul 8184

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

This theorem is used by:  mul31  8457  remulext2  8929  mulreim  8933  mulext2  8942  mulcanapd  8990  mulcanap2d  8991  divcanap1  9012  divrecap2  9020  div23ap  9022  divdivdivap  9044  divmuleqap  9048  divadddivap  9058  apmul2  9120  apdivmuld  9144  divcanap5rd  9149  dmdcanap2d  9152  mvllmulapd  9173  prodgt0  9183  lt2mul2div  9210  mulle0r  9275  subhalfhalf  9542  qapne  10041  irrmulap  10050  mul2lt0llt0  10164  mul2lt0lgt0  10165  mul2lt0pn  10167  modqvalr  10764  modqcyc  10798  mulp1mod1  10804  modqmul12d  10817  modqnegd  10818  modqmulmodr  10829  addmodlteq  10837  expaddzap  11022  binom2  11090  binom3  11096  bccmpl  11194  bcm1k  11200  bcn2  11204  bcpasc  11206  cvg1nlemcxze  11750  cvg1nlemcau  11752  resqrexlemcalc1  11782  resqrexlemcalc2  11783  resqrexlemnm  11786  recvalap  11865  bdtrilem  12007  reccn2ap  12081  isummulc1  12196  fsummulc1  12218  trireciplem  12269  geolim  12280  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  cvgratnnlemfm  12298  cvgratz  12301  mertensabs  12306  eftlub  12459  sinadd  12505  cosadd  12506  sin2t  12518  nndivides  12566  dvds2ln  12593  even2n  12643  oddm1even  12644  m1exp1  12670  divalgmod  12696  bitsp1  12720  bitsinv1lem  12730  mulgcdr  12797  rplpwr  12806  lcmgcdlem  12857  divgcdcoprmex  12882  cncongr1  12883  oddpwdclemxy  12949  2sqpwodd  12956  eulerthlema  13010  eulerthlemth  13012  prmdiv  13015  prmdivdiv  13017  modprmn0modprm0  13037  coprimeprodsq  13038  pythagtriplem6  13051  pythagtriplem7  13052  pceulem  13075  pcadd  13121  prmpwdvds  13136  mul4sqlem  13174  4sqlem17  13188  evenennn  13286  mulgassr  13965  znunit  14996  dvmulxxbr  15805  dvmptcmulcn  15824  dvply1  15868  tangtx  15942  logdivlt  15999  cxpmul  16020  abscxp  16023  binom4  16087  pellexlem2  16098  wilthlem1  16100  mpodvdsmulf1o  16110  sgmppw  16112  perfect1  16118  lgsdirprm  16165  lgsdi  16168  lgsdirnn0  16178  lgsdinn0  16179  gausslemma2dlem1a  16189  gausslemma2dlem6  16198  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad2  16214  2lgslem3a1  16228  2lgslem3b1  16229  2lgslem3c1  16230  2lgslem3d1  16231  2lgsoddprmlem2  16237  2sqlem3  16248  2sqlem4  16249  dichmul0orlem3  16767