Theorem mulcomd 8311

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   · cmul 8148

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

This theorem is referenced by:  mul31  8421  remulext2  8892  mulreim  8896  mulext2  8905  mulcanapd  8953  mulcanap2d  8954  divcanap1  8975  divrecap2  8983  div23ap  8985  divdivdivap  9007  divmuleqap  9011  divadddivap  9021  apmul2  9083  apdivmuld  9107  divcanap5rd  9112  dmdcanap2d  9115  mvllmulapd  9136  prodgt0  9146  lt2mul2div  9173  mulle0r  9238  subhalfhalf  9493  qapne  9992  irrmulap  10001  mul2lt0llt0  10115  mul2lt0lgt0  10116  mul2lt0pn  10118  modqvalr  10714  modqcyc  10748  mulp1mod1  10754  modqmul12d  10767  modqnegd  10768  modqmulmodr  10779  addmodlteq  10787  expaddzap  10972  binom2  11040  binom3  11046  bccmpl  11144  bcm1k  11150  bcn2  11154  bcpasc  11156  cvg1nlemcxze  11695  cvg1nlemcau  11697  resqrexlemcalc1  11727  resqrexlemcalc2  11728  resqrexlemnm  11731  recvalap  11810  bdtrilem  11952  reccn2ap  12026  isummulc1  12141  fsummulc1  12163  trireciplem  12214  geolim  12225  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  cvgratnnlemfm  12243  cvgratz  12246  mertensabs  12251  eftlub  12404  sinadd  12450  cosadd  12451  sin2t  12463  nndivides  12511  dvds2ln  12538  even2n  12588  oddm1even  12589  m1exp1  12615  divalgmod  12641  bitsp1  12665  bitsinv1lem  12675  mulgcdr  12742  rplpwr  12751  lcmgcdlem  12802  divgcdcoprmex  12827  cncongr1  12828  oddpwdclemxy  12894  2sqpwodd  12901  eulerthlema  12955  eulerthlemth  12957  prmdiv  12960  prmdivdiv  12962  modprmn0modprm0  12982  coprimeprodsq  12983  pythagtriplem6  12996  pythagtriplem7  12997  pceulem  13020  pcadd  13066  prmpwdvds  13081  mul4sqlem  13119  4sqlem17  13133  evenennn  13231  mulgassr  13916  znunit  14936  dvmulxxbr  15696  dvmptcmulcn  15715  dvply1  15759  tangtx  15832  cxpmul  15906  abscxp  15909  binom4  15973  pellexlem2  15975  wilthlem1  15977  mpodvdsmulf1o  15987  sgmppw  15989  perfect1  15995  lgsdirprm  16036  lgsdi  16039  lgsdirnn0  16049  lgsdinn0  16050  gausslemma2dlem1a  16060  gausslemma2dlem6  16069  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  lgsquad2  16085  2lgslem3a1  16099  2lgslem3b1  16100  2lgslem3c1  16101  2lgslem3d1  16102  2lgsoddprmlem2  16108  2sqlem3  16119  2sqlem4  16120  dichmul0orlem3  16638