Theorem mulcomd 8136

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

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965   · cmul 7972

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

This theorem is referenced by:  mul31  8245  remulext2  8715  mulreim  8719  mulext2  8728  mulcanapd  8776  mulcanap2d  8777  divcanap1  8796  divrecap2  8804  div23ap  8806  divdivdivap  8828  divmuleqap  8832  divadddivap  8842  apmul2  8904  apdivmuld  8928  divcanap5rd  8933  dmdcanap2d  8936  mvllmulapd  8957  prodgt0  8967  lt2mul2div  8994  mulle0r  9059  subhalfhalf  9314  qapne  9802  irrmulap  9811  mul2lt0llt0  9925  mul2lt0lgt0  9926  mul2lt0pn  9928  modqvalr  10514  modqcyc  10548  mulp1mod1  10554  modqmul12d  10567  modqnegd  10568  modqmulmodr  10579  addmodlteq  10587  expaddzap  10772  binom2  10840  binom3  10846  bccmpl  10943  bcm1k  10949  bcn2  10953  bcpasc  10955  cvg1nlemcxze  11459  cvg1nlemcau  11461  resqrexlemcalc1  11491  resqrexlemcalc2  11492  resqrexlemnm  11495  recvalap  11574  bdtrilem  11716  reccn2ap  11790  isummulc1  11904  fsummulc1  11926  trireciplem  11977  geolim  11988  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  cvgratnnlemfm  12006  cvgratz  12009  mertensabs  12014  eftlub  12167  sinadd  12213  cosadd  12214  sin2t  12226  nndivides  12274  dvds2ln  12301  even2n  12351  oddm1even  12352  m1exp1  12378  divalgmod  12404  bitsp1  12428  bitsinv1lem  12438  mulgcdr  12505  rplpwr  12514  lcmgcdlem  12565  divgcdcoprmex  12590  cncongr1  12591  oddpwdclemxy  12657  2sqpwodd  12664  eulerthlema  12718  eulerthlemth  12720  prmdiv  12723  prmdivdiv  12725  modprmn0modprm0  12745  coprimeprodsq  12746  pythagtriplem6  12759  pythagtriplem7  12760  pceulem  12783  pcadd  12829  prmpwdvds  12844  mul4sqlem  12882  4sqlem17  12896  evenennn  12930  mulgassr  13663  znunit  14588  dvmulxxbr  15341  dvmptcmulcn  15360  dvply1  15404  tangtx  15477  cxpmul  15551  abscxp  15554  binom4  15618  wilthlem1  15619  mpodvdsmulf1o  15629  sgmppw  15631  perfect1  15637  lgsdirprm  15678  lgsdi  15681  lgsdirnn0  15691  lgsdinn0  15692  gausslemma2dlem1a  15702  gausslemma2dlem6  15711  lgsquadlem1  15721  lgsquadlem2  15722  lgsquadlem3  15723  lgsquad2  15727  2lgslem3a1  15741  2lgslem3b1  15742  2lgslem3c1  15743  2lgslem3d1  15744  2lgsoddprmlem2  15750  2sqlem3  15761  2sqlem4  15762