Theorem mulcomd 11154

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025   · cmul 11032

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mul31  11301  mul4r  11303  mulcand  11771  mulcan2d  11772  divcan1  11806  divrec2  11814  div23  11816  divdivdiv  11843  divmuleq  11847  divadddiv  11857  divcan5rd  11945  dmdcan2d  11948  mvllmuld  11974  rdiv  11977  subhalfhalf  12376  mul2lt0llt0  13012  mul2lt0lgt0  13013  prodge0ld  13016  xmulcom  13182  modvalr  13793  mulp1mod1  13835  modmul12d  13849  modnegd  13850  modmulmodr  13861  expaddz  14030  binom3  14148  expmulnbnd  14159  digit1  14161  bccmpl  14233  bcm1k  14239  bcn2  14243  bcpasc  14245  recval  15247  abs1m  15260  bhmafibid1cn  15390  bhmafibid2cn  15391  reccn2  15521  lo1mul2  15553  isummulc1  15687  fsummulc1  15709  incexclem  15760  incexc  15761  trireciplem  15786  pwdif  15792  geolim  15794  cvgrat  15807  mertens  15810  ntrivcvgmul  15826  fallfacfwd  15960  bpoly4  15983  fsumcube  15984  eftlub  16035  sinadd  16090  cosadd  16091  sin2t  16103  nndivides  16190  dvds2ln  16217  even2n  16270  oddm1even  16271  mod2eq1n2dvds  16275  m1exp1  16304  pwp1fsum  16319  divalgmod  16334  bitsp1  16359  bitsinv1lem  16369  sadadd2lem  16387  smumullem  16420  gcdmultiplez  16463  mulgcdr  16478  rplpwr  16486  lcmgcdlem  16534  divgcdcoprmex  16594  cncongr1  16595  eulerthlem2  16710  prmdiv  16713  prmdivdiv  16715  vfermltlALT  16731  modprmn0modprm0  16736  coprimeprodsq  16737  pythagtriplem6  16750  pythagtriplem7  16751  pceulem  16774  pcadd  16818  prmpwdvds  16833  mul4sqlem  16882  4sqlem17  16890  mulgassr  19046  odmodnn0  19473  odmulg  19489  odmulgeq  19490  odbezout  19491  odadd1  19781  ablfacrp2  20002  pgpfac1lem3  20012  zringlpirlem3  21421  znunit  21520  icopnfhmeo  24888  cphassr  25157  pjthlem1  25382  itgabs  25780  dvmulbr  25884  dvcmul  25889  dvcmulf  25890  dvmptcmul  25909  cmvth  25936  cmvthOLD  25937  dvlipcn  25940  c1liplem1  25942  lhop1lem  25959  lhop2  25961  dvcvx  25966  dvfsumlem2  25974  dvfsumlem2OLD  25975  ftc1lem4  25987  itgparts  25995  dvply1  26231  elqaalem3  26269  aalioulem4  26283  taylthlem2  26322  taylthlem2OLD  26323  abelthlem6  26386  abelthlem7  26388  tangtx  26454  tanarg  26568  advlogexp  26604  mulcxp  26634  cxpmul  26637  abscxp  26641  dvcxp2  26690  cxpeq  26707  ang180lem1  26759  lawcoslem1  26765  lawcos  26766  heron  26788  dcubic1  26795  mcubic  26797  cubic2  26798  binom4  26800  dquart  26803  quart1lem  26805  quart1  26806  quartlem1  26807  dvatan  26885  leibpi  26892  log2cnv  26894  efrlim  26919  efrlimOLD  26920  cxp2lim  26927  cxploglim  26928  zetacvg  26965  lgamgulmlem2  26980  lgamgulmlem3  26981  wilthlem1  27018  ftalem1  27023  ftalem5  27027  basellem3  27033  basellem5  27035  mpodvdsmulf1o  27144  dvdsmulf1o  27146  sgmppw  27148  logfac2  27168  chpval2  27169  chpchtsum  27170  perfect1  27179  lgsdirprm  27282  lgsdi  27285  lgsdirnn0  27295  lgsdinn0  27296  gausslemma2dlem1a  27316  gausslemma2dlem6  27323  lgsquadlem1  27331  lgsquadlem2  27332  lgsquadlem3  27333  lgsquad2  27337  2lgslem3a1  27351  2lgslem3b1  27352  2lgslem3c1  27353  2lgslem3d1  27354  2lgsoddprmlem2  27360  2sqlem3  27371  2sqlem4  27372  2sqmod  27387  chebbnd1lem2  27421  chebbnd1lem3  27422  chtppilimlem2  27425  chto1lb  27429  rplogsumlem1  27435  dchrisumlem2  27441  dchrvmasum2lem  27447  dchrisum0flblem2  27460  dchrisum0lem2a  27468  mulogsumlem  27482  mulog2sumlem2  27486  selberglem1  27496  selberg2lem  27501  selberg3lem1  27508  selberg4  27512  pntrsumo1  27516  selberg34r  27522  pntrlog2bndlem3  27530  pntrlog2bndlem4  27531  pntlemb  27548  pntlemq  27552  pntlemr  27553  pntlemj  27554  pntlemo  27558  pnt2  27564  pnt  27565  padicabvcxp  27583  ostth2lem2  27585  ostth2lem3  27586  ostth2lem4  27587  ttgcontlem1  28941  brbtwn2  28962  colinearalglem1  28963  colinearalg  28967  axpaschlem  28997  axcontlem8  29028  numclwwlk1  30420  numclwwlk7  30450  smcnlem  30757  pjhthlem1  31451  kbmul  32015  kbass2  32177  submuladdd  32802  muldivdid  32803  pythagreim  32808  quad3d  32812  sgnmul  32899  2exple2exp  32909  psgnfzto1st  33171  zringfrac  33619  ccfldextdgrr  33822  fldext2rspun  33832  fldext2chn  33878  constrrtlc1  33882  constrrtcclem  33884  constrrtcc  33885  constrremulcl  33917  constrmulcl  33921  cos9thpiminplylem1  33932  qqhval2lem  34131  qqhghm  34138  qqhrhm  34139  oddpwdc  34504  plymulx0  34697  signsvtp  34733  signsvtn  34734  signsvfpn  34735  signsvfnn  34736  breprexplemc  34782  circlemethhgt  34793  logdivsqrle  34800  hgt750lemf  34803  hgt750lemb  34806  hgt750leme  34808  subfacval2  35375  subfaclim  35376  fwddifnp1  36353  knoppndvlem11  36780  knoppndvlem17  36786  bj-subcom  37620  bj-bary1lem1  37623  itg2addnclem  37983  itg2addnclem2  37984  itgabsnc  38001  ftc1cnnclem  38003  areacirclem1  38020  areacirc  38025  geomcau  38071  bfplem1  38134  rrndstprj2  38143  rrnequiv  38147  lcmineqlem1  42460  lcmineqlem5  42464  lcmineqlem8  42467  lcmineqlem11  42470  lcmineqlem18  42477  lcmineqlem21  42480  3lexlogpow5ineq2  42486  3lexlogpow2ineq1  42489  dvrelogpow2b  42499  aks4d1p1p7  42505  primrootscoprmpow  42530  primrootscoprbij  42533  aks6d1c1  42547  aks6d1c2  42561  2np3bcnp1  42575  2ap1caineq  42576  bcle2d  42610  aks6d1c7lem1  42611  nicomachus  42743  retire  42750  readvrec  42793  3cubeslem2  43116  3cubeslem3l  43117  3cubeslem3r  43118  irrapxlem5  43257  pellexlem2  43261  pellexlem6  43265  qirropth  43339  rmxyadd  43352  rmxm1  43365  rmxluc  43367  rmyluc2  43369  rmydbl  43371  jm2.24nn  43390  jm2.17a  43391  jm2.17b  43392  jm2.17c  43393  jm2.18  43419  jm2.19lem2  43421  jm2.22  43426  jm2.23  43427  areaquad  43647  imo72b2  44602  int-mulcomd  44606  int-rightdistd  44610  cvgdvgrat  44743  radcnvrat  44744  bccm1k  44772  binomcxplemwb  44778  binomcxplemnotnn0  44786  sineq0ALT  45366  mul13d  45716  divdiv3d  45792  mccllem  46031  coskpi2  46298  cosknegpi  46301  dvsinax  46345  dvasinbx  46352  dvcosax  46358  dvnxpaek  46374  dvnmul  46375  dvnprodlem2  46379  itgsinexplem1  46386  stoweidlem1  46433  stoweidlem11  46443  stoweidlem26  46458  stoweidlem32  46464  wallispilem4  46500  wallispi2lem1  46503  wallispi2lem2  46504  stirlinglem3  46508  stirlinglem4  46509  stirlinglem5  46510  stirlinglem7  46512  stirlinglem10  46515  stirlinglem15  46520  dirkertrigeqlem1  46530  dirkertrigeqlem2  46531  dirkertrigeqlem3  46532  dirkertrigeq  46533  dirkercncflem1  46535  fourierdlem16  46555  fourierdlem21  46560  fourierdlem22  46561  fourierdlem56  46594  fourierdlem66  46604  fourierdlem83  46621  fourierswlem  46662  fouriersw  46663  etransclem23  46689  etransclem24  46690  etransclem38  46704  etransclem46  46712  hoiprodp1  47020  hoidmvlelem2  47028  smfmullem1  47223  sigarac  47284  sigarls  47289  sigarid  47290  sigardiv  47293  sigarcol  47296  sigaradd  47298  cevathlem1  47299  sqrtnegnre  47741  fmtnoodd  47967  sqrtpwpw2p  47972  fmtnorec3  47982  fmtnoprmfac2lem1  48000  fmtnofac1  48004  lighneallem2  48040  lighneallem3  48041  proththd  48048  requad01  48055  dfeven2  48083  fppr2odd  48165  fpprwppr  48173  altgsumbc  48786  altgsumbcALT  48787  blennnt2  49023  dignn0flhalflem2  49050  dignn0ehalf  49051  itcovalt2lem2lem2  49108  affinecomb2  49137  rrx2linest  49176  itscnhlc0yqe  49193  itsclc0yqsollem1  49196  itscnhlc0xyqsol  49199  itschlc0xyqsol1  49200  itsclc0xyqsolr  49203  itsclquadb  49210  2itscplem3  49214  itscnhlinecirc02plem1  49216  itscnhlinecirc02plem2  49217  inlinecirc02p  49221  amgmwlem  50235