Theorem mulcomd 8341

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   · cmul 8178

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

This theorem is referenced by:  mul31  8451  remulext2  8922  mulreim  8926  mulext2  8935  mulcanapd  8983  mulcanap2d  8984  divcanap1  9005  divrecap2  9013  div23ap  9015  divdivdivap  9037  divmuleqap  9041  divadddivap  9051  apmul2  9113  apdivmuld  9137  divcanap5rd  9142  dmdcanap2d  9145  mvllmulapd  9166  prodgt0  9176  lt2mul2div  9203  mulle0r  9268  subhalfhalf  9523  qapne  10022  irrmulap  10031  mul2lt0llt0  10145  mul2lt0lgt0  10146  mul2lt0pn  10148  modqvalr  10745  modqcyc  10779  mulp1mod1  10785  modqmul12d  10798  modqnegd  10799  modqmulmodr  10810  addmodlteq  10818  expaddzap  11003  binom2  11071  binom3  11077  bccmpl  11175  bcm1k  11181  bcn2  11185  bcpasc  11187  cvg1nlemcxze  11731  cvg1nlemcau  11733  resqrexlemcalc1  11763  resqrexlemcalc2  11764  resqrexlemnm  11767  recvalap  11846  bdtrilem  11988  reccn2ap  12062  isummulc1  12177  fsummulc1  12199  trireciplem  12250  geolim  12261  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  cvgratnnlemfm  12279  cvgratz  12282  mertensabs  12287  eftlub  12440  sinadd  12486  cosadd  12487  sin2t  12499  nndivides  12547  dvds2ln  12574  even2n  12624  oddm1even  12625  m1exp1  12651  divalgmod  12677  bitsp1  12701  bitsinv1lem  12711  mulgcdr  12778  rplpwr  12787  lcmgcdlem  12838  divgcdcoprmex  12863  cncongr1  12864  oddpwdclemxy  12930  2sqpwodd  12937  eulerthlema  12991  eulerthlemth  12993  prmdiv  12996  prmdivdiv  12998  modprmn0modprm0  13018  coprimeprodsq  13019  pythagtriplem6  13032  pythagtriplem7  13033  pceulem  13056  pcadd  13102  prmpwdvds  13117  mul4sqlem  13155  4sqlem17  13169  evenennn  13267  mulgassr  13946  znunit  14977  dvmulxxbr  15786  dvmptcmulcn  15805  dvply1  15849  tangtx  15922  cxpmul  15997  abscxp  16000  binom4  16064  pellexlem2  16075  wilthlem1  16077  mpodvdsmulf1o  16087  sgmppw  16089  perfect1  16095  lgsdirprm  16136  lgsdi  16139  lgsdirnn0  16149  lgsdinn0  16150  gausslemma2dlem1a  16160  gausslemma2dlem6  16169  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad2  16185  2lgslem3a1  16199  2lgslem3b1  16200  2lgslem3c1  16201  2lgslem3d1  16202  2lgsoddprmlem2  16208  2sqlem3  16219  2sqlem4  16220  dichmul0orlem3  16738