Theorem mulcomd 11222

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7396  ℂcc 11095   · cmul 11102

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

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

This theorem is referenced by:  mul31  11368  mul4r  11370  mulcand  11834  mulcan2d  11835  divcan1  11868  divrec2  11876  div23  11878  divdivdiv  11902  divmuleq  11906  divadddiv  11916  divcan5rd  12004  dmdcan2d  12007  mvllmuld  12033  rdiv  12036  subhalfhalf  12433  mul2lt0llt0  13065  mul2lt0lgt0  13066  prodge0ld  13069  xmulcom  13232  modvalr  13824  mulp1mod1  13864  modmul12d  13877  modnegd  13878  modmulmodr  13889  expaddz  14059  binom3  14174  expmulnbnd  14185  digit1  14187  bccmpl  14256  bcm1k  14262  bcn2  14266  bcpasc  14268  recval  15256  abs1m  15269  bhmafibid1cn  15397  bhmafibid2cn  15398  reccn2  15528  lo1mul2  15560  isummulc1  15696  fsummulc1  15718  incexclem  15769  incexc  15770  trireciplem  15795  pwdif  15801  geolim  15803  cvgrat  15816  mertens  15819  ntrivcvgmul  15835  fallfacfwd  15967  bpoly4  15990  fsumcube  15991  eftlub  16039  sinadd  16094  cosadd  16095  sin2t  16107  nndivides  16194  dvds2ln  16219  even2n  16272  oddm1even  16273  mod2eq1n2dvds  16277  m1exp1  16306  pwp1fsum  16321  divalgmod  16336  bitsp1  16359  bitsinv1lem  16369  sadadd2lem  16387  smumullem  16420  gcdmultiplez  16464  mulgcdr  16479  rplpwr  16486  lcmgcdlem  16530  divgcdcoprmex  16590  cncongr1  16591  eulerthlem2  16702  prmdiv  16705  prmdivdiv  16707  vfermltlALT  16722  modprmn0modprm0  16727  coprimeprodsq  16728  pythagtriplem6  16741  pythagtriplem7  16742  pceulem  16765  pcadd  16809  prmpwdvds  16824  mul4sqlem  16873  4sqlem17  16881  mulgassr  18977  odmodnn0  19392  odmulg  19408  odmulgeq  19409  odbezout  19410  odadd1  19699  ablfacrp2  19920  pgpfac1lem3  19930  zringlpirlem3  21007  znunit  21092  icopnfhmeo  24428  cphassr  24698  pjthlem1  24923  itgabs  25321  dvmulbr  25425  dvcmul  25430  dvcmulf  25431  dvmptcmul  25450  cmvth  25477  dvlipcn  25480  c1liplem1  25482  lhop1lem  25499  lhop2  25501  dvcvx  25506  dvfsumlem2  25513  ftc1lem4  25525  itgparts  25533  dvply1  25766  elqaalem3  25803  aalioulem4  25817  taylthlem2  25855  abelthlem6  25917  abelthlem7  25919  tangtx  25984  tanarg  26096  advlogexp  26132  mulcxp  26162  cxpmul  26165  abscxp  26169  dvcxp2  26216  cxpeq  26232  ang180lem1  26281  lawcoslem1  26287  lawcos  26288  heron  26310  dcubic1  26317  mcubic  26319  cubic2  26320  binom4  26322  dquart  26325  quart1lem  26327  quart1  26328  quartlem1  26329  dvatan  26407  leibpi  26414  log2cnv  26416  efrlim  26441  cxp2lim  26448  cxploglim  26449  zetacvg  26486  lgamgulmlem2  26501  lgamgulmlem3  26502  wilthlem1  26539  ftalem1  26544  ftalem5  26548  basellem3  26554  basellem5  26556  dvdsmulf1o  26665  sgmppw  26667  logfac2  26687  chpval2  26688  chpchtsum  26689  perfect1  26698  lgsdirprm  26801  lgsdi  26804  lgsdirnn0  26814  lgsdinn0  26815  gausslemma2dlem1a  26835  gausslemma2dlem6  26842  lgsquadlem1  26850  lgsquadlem2  26851  lgsquadlem3  26852  lgsquad2  26856  2lgslem3a1  26870  2lgslem3b1  26871  2lgslem3c1  26872  2lgslem3d1  26873  2lgsoddprmlem2  26879  2sqlem3  26890  2sqlem4  26891  2sqmod  26906  chebbnd1lem2  26940  chebbnd1lem3  26941  chtppilimlem2  26944  chto1lb  26948  rplogsumlem1  26954  dchrisumlem2  26960  dchrvmasum2lem  26966  dchrisum0flblem2  26979  dchrisum0lem2a  26987  mulogsumlem  27001  mulog2sumlem2  27005  selberglem1  27015  selberg2lem  27020  selberg3lem1  27027  selberg4  27031  pntrsumo1  27035  selberg34r  27041  pntrlog2bndlem3  27049  pntrlog2bndlem4  27050  pntlemb  27067  pntlemq  27071  pntlemr  27072  pntlemj  27073  pntlemo  27077  pnt2  27083  pnt  27084  padicabvcxp  27102  ostth2lem2  27104  ostth2lem3  27105  ostth2lem4  27106  ttgcontlem1  28109  brbtwn2  28130  colinearalglem1  28131  colinearalg  28135  axpaschlem  28165  axcontlem8  28196  numclwwlk1  29581  numclwwlk7  29611  smcnlem  29915  pjhthlem1  30609  kbmul  31173  kbass2  31335  psgnfzto1st  32235  ccfldextdgrr  32684  qqhval2lem  32892  qqhghm  32899  qqhrhm  32900  oddpwdc  33284  sgnmul  33472  plymulx0  33489  signsvtp  33525  signsvtn  33526  signsvfpn  33527  signsvfnn  33528  breprexplemc  33575  circlemethhgt  33586  logdivsqrle  33593  hgt750lemf  33596  hgt750lemb  33599  hgt750leme  33601  subfacval2  34109  subfaclim  34110  fwddifnp1  35068  knoppndvlem11  35303  knoppndvlem17  35309  bj-subcom  36094  bj-bary1lem1  36097  itg2addnclem  36444  itg2addnclem2  36445  itgabsnc  36462  ftc1cnnclem  36464  areacirclem1  36481  areacirc  36486  geomcau  36533  bfplem1  36596  rrndstprj2  36605  rrnequiv  36609  lcmineqlem1  40800  lcmineqlem5  40804  lcmineqlem8  40807  lcmineqlem11  40810  lcmineqlem18  40817  lcmineqlem21  40820  3lexlogpow5ineq2  40826  3lexlogpow2ineq1  40829  dvrelogpow2b  40839  aks4d1p1p7  40845  2np3bcnp1  40866  2ap1caineq  40867  3cubeslem2  41294  3cubeslem3l  41295  3cubeslem3r  41296  irrapxlem5  41435  pellexlem2  41439  pellexlem6  41443  qirropth  41517  rmxyadd  41531  rmxm1  41544  rmxluc  41546  rmyluc2  41548  rmydbl  41550  jm2.24nn  41569  jm2.17a  41570  jm2.17b  41571  jm2.17c  41572  jm2.18  41598  jm2.19lem2  41600  jm2.22  41605  jm2.23  41606  areaquad  41836  imo72b2  42795  int-mulcomd  42799  int-rightdistd  42803  cvgdvgrat  42943  radcnvrat  42944  bccm1k  42972  binomcxplemwb  42978  binomcxplemnotnn0  42986  sineq0ALT  43569  mul13d  43862  divdiv3d  43942  mccllem  44186  coskpi2  44455  cosknegpi  44458  dvsinax  44502  dvasinbx  44509  dvcosax  44515  dvnxpaek  44531  dvnmul  44532  dvnprodlem2  44536  itgsinexplem1  44543  stoweidlem1  44590  stoweidlem11  44600  stoweidlem26  44615  stoweidlem32  44621  wallispilem4  44657  wallispi2lem1  44660  wallispi2lem2  44661  stirlinglem3  44665  stirlinglem4  44666  stirlinglem5  44667  stirlinglem7  44669  stirlinglem10  44672  stirlinglem15  44677  dirkertrigeqlem1  44687  dirkertrigeqlem2  44688  dirkertrigeqlem3  44689  dirkertrigeq  44690  dirkercncflem1  44692  fourierdlem16  44712  fourierdlem21  44717  fourierdlem22  44718  fourierdlem56  44751  fourierdlem66  44761  fourierdlem83  44778  fourierswlem  44819  fouriersw  44820  etransclem23  44846  etransclem24  44847  etransclem38  44861  etransclem46  44869  hoiprodp1  45177  hoidmvlelem2  45185  smfmullem1  45380  sigarac  45441  sigarls  45446  sigarid  45447  sigardiv  45450  sigarcol  45453  sigaradd  45455  cevathlem1  45456  sqrtnegnre  45888  fmtnoodd  46074  sqrtpwpw2p  46079  fmtnorec3  46089  fmtnoprmfac2lem1  46107  fmtnofac1  46111  lighneallem2  46147  lighneallem3  46148  proththd  46155  requad01  46162  dfeven2  46190  fppr2odd  46272  fpprwppr  46280  altgsumbc  46868  altgsumbcALT  46869  blennnt2  47115  dignn0flhalflem2  47142  dignn0ehalf  47143  itcovalt2lem2lem2  47200  affinecomb2  47229  rrx2linest  47268  itscnhlc0yqe  47285  itsclc0yqsollem1  47288  itscnhlc0xyqsol  47291  itschlc0xyqsol1  47292  itsclc0xyqsolr  47295  itsclquadb  47302  2itscplem3  47306  itscnhlinecirc02plem1  47308  itscnhlinecirc02plem2  47309  inlinecirc02p  47313  amgmwlem  47689