Theorem mulcomd 11176

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7357  ℂcc 11049   · cmul 11056

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

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

This theorem is referenced by:  mul31  11322  mul4r  11324  mulcand  11788  mulcan2d  11789  divcan1  11822  divrec2  11830  div23  11832  divdivdiv  11856  divmuleq  11860  divadddiv  11870  divcan5rd  11958  dmdcan2d  11961  mvllmuld  11987  rdiv  11990  subhalfhalf  12387  mul2lt0llt0  13019  mul2lt0lgt0  13020  prodge0ld  13023  xmulcom  13185  modvalr  13777  mulp1mod1  13817  modmul12d  13830  modnegd  13831  modmulmodr  13842  expaddz  14012  binom3  14127  expmulnbnd  14138  digit1  14140  bccmpl  14209  bcm1k  14215  bcn2  14219  bcpasc  14221  recval  15207  abs1m  15220  bhmafibid1cn  15348  bhmafibid2cn  15349  reccn2  15479  lo1mul2  15511  isummulc1  15648  fsummulc1  15670  incexclem  15721  incexc  15722  trireciplem  15747  pwdif  15753  geolim  15755  cvgrat  15768  mertens  15771  ntrivcvgmul  15787  fallfacfwd  15919  bpoly4  15942  fsumcube  15943  eftlub  15991  sinadd  16046  cosadd  16047  sin2t  16059  nndivides  16146  dvds2ln  16171  even2n  16224  oddm1even  16225  mod2eq1n2dvds  16229  m1exp1  16258  pwp1fsum  16273  divalgmod  16288  bitsp1  16311  bitsinv1lem  16321  sadadd2lem  16339  smumullem  16372  gcdmultiplez  16416  mulgcdr  16431  rplpwr  16438  lcmgcdlem  16482  divgcdcoprmex  16542  cncongr1  16543  eulerthlem2  16654  prmdiv  16657  prmdivdiv  16659  vfermltlALT  16674  modprmn0modprm0  16679  coprimeprodsq  16680  pythagtriplem6  16693  pythagtriplem7  16694  pceulem  16717  pcadd  16761  prmpwdvds  16776  mul4sqlem  16825  4sqlem17  16833  mulgassr  18914  odmodnn0  19322  odmulg  19338  odmulgeq  19339  odbezout  19340  odadd1  19626  ablfacrp2  19846  pgpfac1lem3  19856  zringlpirlem3  20885  znunit  20970  icopnfhmeo  24306  cphassr  24576  pjthlem1  24801  itgabs  25199  dvmulbr  25303  dvcmul  25308  dvcmulf  25309  dvmptcmul  25328  cmvth  25355  dvlipcn  25358  c1liplem1  25360  lhop1lem  25377  lhop2  25379  dvcvx  25384  dvfsumlem2  25391  ftc1lem4  25403  itgparts  25411  dvply1  25644  elqaalem3  25681  aalioulem4  25695  taylthlem2  25733  abelthlem6  25795  abelthlem7  25797  tangtx  25862  tanarg  25974  advlogexp  26010  mulcxp  26040  cxpmul  26043  abscxp  26047  dvcxp2  26094  cxpeq  26110  ang180lem1  26159  lawcoslem1  26165  lawcos  26166  heron  26188  dcubic1  26195  mcubic  26197  cubic2  26198  binom4  26200  dquart  26203  quart1lem  26205  quart1  26206  quartlem1  26207  dvatan  26285  leibpi  26292  log2cnv  26294  efrlim  26319  cxp2lim  26326  cxploglim  26327  zetacvg  26364  lgamgulmlem2  26379  lgamgulmlem3  26380  wilthlem1  26417  ftalem1  26422  ftalem5  26426  basellem3  26432  basellem5  26434  dvdsmulf1o  26543  sgmppw  26545  logfac2  26565  chpval2  26566  chpchtsum  26567  perfect1  26576  lgsdirprm  26679  lgsdi  26682  lgsdirnn0  26692  lgsdinn0  26693  gausslemma2dlem1a  26713  gausslemma2dlem6  26720  lgsquadlem1  26728  lgsquadlem2  26729  lgsquadlem3  26730  lgsquad2  26734  2lgslem3a1  26748  2lgslem3b1  26749  2lgslem3c1  26750  2lgslem3d1  26751  2lgsoddprmlem2  26757  2sqlem3  26768  2sqlem4  26769  2sqmod  26784  chebbnd1lem2  26818  chebbnd1lem3  26819  chtppilimlem2  26822  chto1lb  26826  rplogsumlem1  26832  dchrisumlem2  26838  dchrvmasum2lem  26844  dchrisum0flblem2  26857  dchrisum0lem2a  26865  mulogsumlem  26879  mulog2sumlem2  26883  selberglem1  26893  selberg2lem  26898  selberg3lem1  26905  selberg4  26909  pntrsumo1  26913  selberg34r  26919  pntrlog2bndlem3  26927  pntrlog2bndlem4  26928  pntlemb  26945  pntlemq  26949  pntlemr  26950  pntlemj  26951  pntlemo  26955  pnt2  26961  pnt  26962  padicabvcxp  26980  ostth2lem2  26982  ostth2lem3  26983  ostth2lem4  26984  ttgcontlem1  27833  brbtwn2  27854  colinearalglem1  27855  colinearalg  27859  axpaschlem  27889  axcontlem8  27920  numclwwlk1  29305  numclwwlk7  29335  smcnlem  29639  pjhthlem1  30333  kbmul  30897  kbass2  31059  psgnfzto1st  31954  ccfldextdgrr  32356  qqhval2lem  32562  qqhghm  32569  qqhrhm  32570  oddpwdc  32954  sgnmul  33142  plymulx0  33159  signsvtp  33195  signsvtn  33196  signsvfpn  33197  signsvfnn  33198  breprexplemc  33245  circlemethhgt  33256  logdivsqrle  33263  hgt750lemf  33266  hgt750lemb  33269  hgt750leme  33271  subfacval2  33781  subfaclim  33782  fwddifnp1  34750  knoppndvlem11  34985  knoppndvlem17  34991  bj-subcom  35779  bj-bary1lem1  35782  itg2addnclem  36129  itg2addnclem2  36130  itgabsnc  36147  ftc1cnnclem  36149  areacirclem1  36166  areacirc  36171  geomcau  36218  bfplem1  36281  rrndstprj2  36290  rrnequiv  36294  lcmineqlem1  40486  lcmineqlem5  40490  lcmineqlem8  40493  lcmineqlem11  40496  lcmineqlem18  40503  lcmineqlem21  40506  3lexlogpow5ineq2  40512  3lexlogpow2ineq1  40515  dvrelogpow2b  40525  aks4d1p1p7  40531  2np3bcnp1  40552  2ap1caineq  40553  3cubeslem2  40994  3cubeslem3l  40995  3cubeslem3r  40996  irrapxlem5  41135  pellexlem2  41139  pellexlem6  41143  qirropth  41217  rmxyadd  41231  rmxm1  41244  rmxluc  41246  rmyluc2  41248  rmydbl  41250  jm2.24nn  41269  jm2.17a  41270  jm2.17b  41271  jm2.17c  41272  jm2.18  41298  jm2.19lem2  41300  jm2.22  41305  jm2.23  41306  areaquad  41536  imo72b2  42435  int-mulcomd  42439  int-rightdistd  42443  cvgdvgrat  42583  radcnvrat  42584  bccm1k  42612  binomcxplemwb  42618  binomcxplemnotnn0  42626  sineq0ALT  43209  mul13d  43503  divdiv3d  43583  mccllem  43828  coskpi2  44097  cosknegpi  44100  dvsinax  44144  dvasinbx  44151  dvcosax  44157  dvnxpaek  44173  dvnmul  44174  dvnprodlem2  44178  itgsinexplem1  44185  stoweidlem1  44232  stoweidlem11  44242  stoweidlem26  44257  stoweidlem32  44263  wallispilem4  44299  wallispi2lem1  44302  wallispi2lem2  44303  stirlinglem3  44307  stirlinglem4  44308  stirlinglem5  44309  stirlinglem7  44311  stirlinglem10  44314  stirlinglem15  44319  dirkertrigeqlem1  44329  dirkertrigeqlem2  44330  dirkertrigeqlem3  44331  dirkertrigeq  44332  dirkercncflem1  44334  fourierdlem16  44354  fourierdlem21  44359  fourierdlem22  44360  fourierdlem56  44393  fourierdlem66  44403  fourierdlem83  44420  fourierswlem  44461  fouriersw  44462  etransclem23  44488  etransclem24  44489  etransclem38  44503  etransclem46  44511  hoiprodp1  44819  hoidmvlelem2  44827  smfmullem1  45022  sigarac  45083  sigarls  45088  sigarid  45089  sigardiv  45092  sigarcol  45095  sigaradd  45097  cevathlem1  45098  sqrtnegnre  45529  fmtnoodd  45715  sqrtpwpw2p  45720  fmtnorec3  45730  fmtnoprmfac2lem1  45748  fmtnofac1  45752  lighneallem2  45788  lighneallem3  45789  proththd  45796  requad01  45803  dfeven2  45831  fppr2odd  45913  fpprwppr  45921  altgsumbc  46418  altgsumbcALT  46419  blennnt2  46665  dignn0flhalflem2  46692  dignn0ehalf  46693  itcovalt2lem2lem2  46750  affinecomb2  46779  rrx2linest  46818  itscnhlc0yqe  46835  itsclc0yqsollem1  46838  itscnhlc0xyqsol  46841  itschlc0xyqsol1  46842  itsclc0xyqsolr  46845  itsclquadb  46852  2itscplem3  46856  itscnhlinecirc02plem1  46858  itscnhlinecirc02plem2  46859  inlinecirc02p  46863  amgmwlem  47239