Theorem mulcomd 11185

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7362  ℂcc 11058   · cmul 11065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 11124

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  mul31  11331  mul4r  11333  mulcand  11797  mulcan2d  11798  divcan1  11831  divrec2  11839  div23  11841  divdivdiv  11865  divmuleq  11869  divadddiv  11879  divcan5rd  11967  dmdcan2d  11970  mvllmuld  11996  rdiv  11999  subhalfhalf  12396  mul2lt0llt0  13028  mul2lt0lgt0  13029  prodge0ld  13032  xmulcom  13195  modvalr  13787  mulp1mod1  13827  modmul12d  13840  modnegd  13841  modmulmodr  13852  expaddz  14022  binom3  14137  expmulnbnd  14148  digit1  14150  bccmpl  14219  bcm1k  14225  bcn2  14229  bcpasc  14231  recval  15219  abs1m  15232  bhmafibid1cn  15360  bhmafibid2cn  15361  reccn2  15491  lo1mul2  15523  isummulc1  15659  fsummulc1  15681  incexclem  15732  incexc  15733  trireciplem  15758  pwdif  15764  geolim  15766  cvgrat  15779  mertens  15782  ntrivcvgmul  15798  fallfacfwd  15930  bpoly4  15953  fsumcube  15954  eftlub  16002  sinadd  16057  cosadd  16058  sin2t  16070  nndivides  16157  dvds2ln  16182  even2n  16235  oddm1even  16236  mod2eq1n2dvds  16240  m1exp1  16269  pwp1fsum  16284  divalgmod  16299  bitsp1  16322  bitsinv1lem  16332  sadadd2lem  16350  smumullem  16383  gcdmultiplez  16427  mulgcdr  16442  rplpwr  16449  lcmgcdlem  16493  divgcdcoprmex  16553  cncongr1  16554  eulerthlem2  16665  prmdiv  16668  prmdivdiv  16670  vfermltlALT  16685  modprmn0modprm0  16690  coprimeprodsq  16691  pythagtriplem6  16704  pythagtriplem7  16705  pceulem  16728  pcadd  16772  prmpwdvds  16787  mul4sqlem  16836  4sqlem17  16844  mulgassr  18928  odmodnn0  19336  odmulg  19352  odmulgeq  19353  odbezout  19354  odadd1  19640  ablfacrp2  19860  pgpfac1lem3  19870  zringlpirlem3  20922  znunit  21007  icopnfhmeo  24343  cphassr  24613  pjthlem1  24838  itgabs  25236  dvmulbr  25340  dvcmul  25345  dvcmulf  25346  dvmptcmul  25365  cmvth  25392  dvlipcn  25395  c1liplem1  25397  lhop1lem  25414  lhop2  25416  dvcvx  25421  dvfsumlem2  25428  ftc1lem4  25440  itgparts  25448  dvply1  25681  elqaalem3  25718  aalioulem4  25732  taylthlem2  25770  abelthlem6  25832  abelthlem7  25834  tangtx  25899  tanarg  26011  advlogexp  26047  mulcxp  26077  cxpmul  26080  abscxp  26084  dvcxp2  26131  cxpeq  26147  ang180lem1  26196  lawcoslem1  26202  lawcos  26203  heron  26225  dcubic1  26232  mcubic  26234  cubic2  26235  binom4  26237  dquart  26240  quart1lem  26242  quart1  26243  quartlem1  26244  dvatan  26322  leibpi  26329  log2cnv  26331  efrlim  26356  cxp2lim  26363  cxploglim  26364  zetacvg  26401  lgamgulmlem2  26416  lgamgulmlem3  26417  wilthlem1  26454  ftalem1  26459  ftalem5  26463  basellem3  26469  basellem5  26471  dvdsmulf1o  26580  sgmppw  26582  logfac2  26602  chpval2  26603  chpchtsum  26604  perfect1  26613  lgsdirprm  26716  lgsdi  26719  lgsdirnn0  26729  lgsdinn0  26730  gausslemma2dlem1a  26750  gausslemma2dlem6  26757  lgsquadlem1  26765  lgsquadlem2  26766  lgsquadlem3  26767  lgsquad2  26771  2lgslem3a1  26785  2lgslem3b1  26786  2lgslem3c1  26787  2lgslem3d1  26788  2lgsoddprmlem2  26794  2sqlem3  26805  2sqlem4  26806  2sqmod  26821  chebbnd1lem2  26855  chebbnd1lem3  26856  chtppilimlem2  26859  chto1lb  26863  rplogsumlem1  26869  dchrisumlem2  26875  dchrvmasum2lem  26881  dchrisum0flblem2  26894  dchrisum0lem2a  26902  mulogsumlem  26916  mulog2sumlem2  26920  selberglem1  26930  selberg2lem  26935  selberg3lem1  26942  selberg4  26946  pntrsumo1  26950  selberg34r  26956  pntrlog2bndlem3  26964  pntrlog2bndlem4  26965  pntlemb  26982  pntlemq  26986  pntlemr  26987  pntlemj  26988  pntlemo  26992  pnt2  26998  pnt  26999  padicabvcxp  27017  ostth2lem2  27019  ostth2lem3  27020  ostth2lem4  27021  ttgcontlem1  27896  brbtwn2  27917  colinearalglem1  27918  colinearalg  27922  axpaschlem  27952  axcontlem8  27983  numclwwlk1  29368  numclwwlk7  29398  smcnlem  29702  pjhthlem1  30396  kbmul  30960  kbass2  31122  psgnfzto1st  32024  ccfldextdgrr  32443  qqhval2lem  32651  qqhghm  32658  qqhrhm  32659  oddpwdc  33043  sgnmul  33231  plymulx0  33248  signsvtp  33284  signsvtn  33285  signsvfpn  33286  signsvfnn  33287  breprexplemc  33334  circlemethhgt  33345  logdivsqrle  33352  hgt750lemf  33355  hgt750lemb  33358  hgt750leme  33360  subfacval2  33868  subfaclim  33869  fwddifnp1  34826  knoppndvlem11  35061  knoppndvlem17  35067  bj-subcom  35852  bj-bary1lem1  35855  itg2addnclem  36202  itg2addnclem2  36203  itgabsnc  36220  ftc1cnnclem  36222  areacirclem1  36239  areacirc  36244  geomcau  36291  bfplem1  36354  rrndstprj2  36363  rrnequiv  36367  lcmineqlem1  40559  lcmineqlem5  40563  lcmineqlem8  40566  lcmineqlem11  40569  lcmineqlem18  40576  lcmineqlem21  40579  3lexlogpow5ineq2  40585  3lexlogpow2ineq1  40588  dvrelogpow2b  40598  aks4d1p1p7  40604  2np3bcnp1  40625  2ap1caineq  40626  3cubeslem2  41066  3cubeslem3l  41067  3cubeslem3r  41068  irrapxlem5  41207  pellexlem2  41211  pellexlem6  41215  qirropth  41289  rmxyadd  41303  rmxm1  41316  rmxluc  41318  rmyluc2  41320  rmydbl  41322  jm2.24nn  41341  jm2.17a  41342  jm2.17b  41343  jm2.17c  41344  jm2.18  41370  jm2.19lem2  41372  jm2.22  41377  jm2.23  41378  areaquad  41608  imo72b2  42567  int-mulcomd  42571  int-rightdistd  42575  cvgdvgrat  42715  radcnvrat  42716  bccm1k  42744  binomcxplemwb  42750  binomcxplemnotnn0  42758  sineq0ALT  43341  mul13d  43634  divdiv3d  43714  mccllem  43958  coskpi2  44227  cosknegpi  44230  dvsinax  44274  dvasinbx  44281  dvcosax  44287  dvnxpaek  44303  dvnmul  44304  dvnprodlem2  44308  itgsinexplem1  44315  stoweidlem1  44362  stoweidlem11  44372  stoweidlem26  44387  stoweidlem32  44393  wallispilem4  44429  wallispi2lem1  44432  wallispi2lem2  44433  stirlinglem3  44437  stirlinglem4  44438  stirlinglem5  44439  stirlinglem7  44441  stirlinglem10  44444  stirlinglem15  44449  dirkertrigeqlem1  44459  dirkertrigeqlem2  44460  dirkertrigeqlem3  44461  dirkertrigeq  44462  dirkercncflem1  44464  fourierdlem16  44484  fourierdlem21  44489  fourierdlem22  44490  fourierdlem56  44523  fourierdlem66  44533  fourierdlem83  44550  fourierswlem  44591  fouriersw  44592  etransclem23  44618  etransclem24  44619  etransclem38  44633  etransclem46  44641  hoiprodp1  44949  hoidmvlelem2  44957  smfmullem1  45152  sigarac  45213  sigarls  45218  sigarid  45219  sigardiv  45222  sigarcol  45225  sigaradd  45227  cevathlem1  45228  sqrtnegnre  45659  fmtnoodd  45845  sqrtpwpw2p  45850  fmtnorec3  45860  fmtnoprmfac2lem1  45878  fmtnofac1  45882  lighneallem2  45918  lighneallem3  45919  proththd  45926  requad01  45933  dfeven2  45961  fppr2odd  46043  fpprwppr  46051  altgsumbc  46548  altgsumbcALT  46549  blennnt2  46795  dignn0flhalflem2  46822  dignn0ehalf  46823  itcovalt2lem2lem2  46880  affinecomb2  46909  rrx2linest  46948  itscnhlc0yqe  46965  itsclc0yqsollem1  46968  itscnhlc0xyqsol  46971  itschlc0xyqsol1  46972  itsclc0xyqsolr  46975  itsclquadb  46982  2itscplem3  46986  itscnhlinecirc02plem1  46988  itscnhlinecirc02plem2  46989  inlinecirc02p  46993  amgmwlem  47369