Theorem mulcomd 11330

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198   · cmul 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 11264

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mul31  11477  mul4r  11479  mulcand  11949  mulcan2d  11950  divcan1  11983  divrec2  11991  div23  11993  muldivdid  12011  divdivdiv  12018  divmuleq  12022  divadddiv  12032  divcan5rd  12120  dmdcan2d  12123  mvllmuld  12149  rdiv  12152  subhalfhalf  12580  mul2lt0llt0  13226  mul2lt0lgt0  13227  prodge0ld  13230  xmulcom  13396  modvalr  14012  mulp1mod1  14054  modmul12d  14068  modnegd  14069  modmulmodr  14080  expaddz  14249  binom3  14368  expmulnbnd  14379  digit1  14381  bccmpl  14453  bcm1k  14459  bcn2  14463  bcpasc  14465  sgnmul  15260  recval  15490  abs1m  15503  bhmafibid1cn  15633  bhmafibid2cn  15634  reccn2  15764  lo1mul2  15796  isummulc1  15929  fsummulc1  15951  incexclem  16005  incexc  16006  trireciplem  16031  pwdif  16037  geolim  16039  cvgrat  16052  mertens  16055  ntrivcvgmul  16071  fallfacfwd  16202  bpoly4  16225  fsumcube  16226  eftlub  16277  sinadd  16332  cosadd  16333  sin2t  16345  nndivides  16432  dvds2ln  16459  even2n  16512  oddm1even  16513  mod2eq1n2dvds  16517  m1exp1  16546  pwp1fsum  16561  divalgmod  16576  bitsp1  16601  bitsinv1lem  16611  sadadd2lem  16629  smumullem  16662  gcdmultiplez  16708  mulgcdr  16723  rplpwr  16732  lcmgcdlem  16781  divgcdcoprmex  16841  cncongr1  16842  eulerthlem2  16959  prmdiv  16962  prmdivdiv  16964  vfermltlALT  16980  modprmn0modprm0  16985  coprimeprodsq  16986  pythagtriplem6  16999  pythagtriplem7  17000  pceulem  17023  pcadd  17067  prmpwdvds  17082  mul4sqlem  17131  4sqlem17  17139  mulgassr  19322  odmodnn0  19754  odmulg  19770  odmulgeq  19771  odbezout  19772  odadd1  20062  ablfacrp2  20283  pgpfac1lem3  20293  zringlpirlem3  21770  znunit  21869  icopnfhmeo  25264  cphassr  25533  pjthlem1  25758  itgabs  26155  dvmulbr  26259  dvcmul  26264  dvcmulf  26265  dvmptcmul  26284  cmvth  26311  dvlipcn  26314  c1liplem1  26316  lhop1lem  26333  lhop2  26335  dvcvx  26340  dvfsumlem2  26347  ftc1lem4  26359  itgparts  26367  plyn0mulidp  26602  dvply1  26605  elqaalem3  26644  aalioulem4  26662  taylthlem2  26701  abelthlem6  26763  abelthlem7  26765  tangtx  26834  tanarg  26947  advlogexp  26983  mulcxp  27013  cxpmul  27016  abscxp  27020  dvcxp2  27069  cxpeq  27085  ang180lem1  27137  lawcoslem1  27143  lawcos  27144  heron  27166  dcubic1  27173  mcubic  27175  cubic2  27176  binom4  27178  dquart  27181  quart1lem  27183  quart1  27184  quartlem1  27185  dvatan  27263  leibpi  27270  log2cnv  27272  efrlim  27297  cxp2lim  27304  cxploglim  27305  zetacvg  27342  lgamgulmlem2  27357  lgamgulmlem3  27358  wilthlem1  27395  ftalem1  27400  ftalem5  27404  basellem3  27410  basellem5  27412  basellem8  27415  mpodvdsmulf1o  27521  dvdsmulf1o  27523  sgmppw  27524  logfac2  27544  chpval2  27545  chpchtsum  27546  perfect1  27555  lgsdirprm  27658  lgsdi  27661  lgsdirnn0  27671  lgsdinn0  27672  gausslemma2dlem1a  27692  gausslemma2dlem6  27699  lgsquadlem1  27707  lgsquadlem2  27708  lgsquadlem3  27709  lgsquad2  27713  2lgslem3a1  27727  2lgslem3b1  27728  2lgslem3c1  27729  2lgslem3d1  27730  2lgsoddprmlem2  27736  2sqlem3  27747  2sqlem4  27748  2sqmod  27763  chebbnd1lem2  27797  chebbnd1lem3  27798  chtppilimlem2  27801  chto1lb  27805  rplogsumlem1  27811  dchrisumlem2  27817  dchrvmasum2lem  27823  dchrisum0flblem2  27836  dchrisum0lem2a  27844  mulogsumlem  27858  mulog2sumlem2  27862  selberglem1  27872  selberg2lem  27877  selberg3lem1  27884  selberg4  27888  pntrsumo1  27892  selberg34r  27898  pntrlog2bndlem3  27906  pntrlog2bndlem4  27907  pntlemb  27924  pntlemq  27928  pntlemr  27929  pntlemj  27930  pntlemo  27934  pnt2  27940  pnt  27941  padicabvcxp  27959  ostth2lem2  27961  ostth2lem3  27962  ostth2lem4  27963  ttgcontlem1  29462  brbtwn2  29483  colinearalglem1  29484  colinearalg  29488  axpaschlem  29518  axcontlem8  29549  numclwwlk1  30962  numclwwlk7  30992  smcnlem  31299  pjhthlem1  31993  kbmul  32557  kbass2  32719  submuladdd  33332  pythagreim  33337  quad3d  33341  2exple2exp  33425  psgnfzto1st  33666  zringfrac  34086  ccfldextdgrr  34304  fldext2rspun  34314  fldext2chn  34360  constrrtlc1  34364  constrrtcclem  34366  constrrtcc  34367  constrremulcl  34399  constrmulcl  34403  cos9thpiminplylem1  34414  qqhval2lem  34613  qqhghm  34620  qqhrhm  34621  oddpwdc  34986  signsvtp  35212  signsvtn  35213  signsvfpn  35214  signsvfnn  35215  breprexplemc  35261  circlemethhgt  35272  logdivsqrle  35279  hgt750lemf  35282  hgt750lemb  35285  hgt750leme  35287  subfacval2  35952  subfaclim  35953  fwddifnp1  36930  knoppndvlem11  37388  knoppndvlem17  37394  bj-subcom  38229  bj-bary1lem1  38232  itg2addnclem  38589  itg2addnclem2  38590  itgabsnc  38607  ftc1cnnclem  38609  areacirclem1  38626  areacirc  38631  geomcau  38693  bfplem1  38756  rrndstprj2  38765  rrnequiv  38769  lcmineqlem1  43079  lcmineqlem5  43083  lcmineqlem8  43086  lcmineqlem11  43089  lcmineqlem18  43096  lcmineqlem21  43099  3lexlogpow5ineq2  43105  3lexlogpow2ineq1  43108  dvrelogpow2b  43118  aks4d1p1p7  43124  primrootscoprmpow  43149  primrootscoprbij  43152  aks6d1c1  43166  aks6d1c2  43180  2np3bcnp1  43194  2ap1caineq  43195  bcle2d  43229  aks6d1c7lem1  43230  quadfac  43255  nicomachus  43369  retire  43376  readvrec  43413  3cubeslem2  43695  3cubeslem3l  43696  3cubeslem3r  43697  irrapxlem5  43832  pellexlem2  43836  pellexlem6  43840  qirropth  43914  rmxyadd  43927  rmxm1  43940  rmxluc  43942  rmyluc2  43944  rmydbl  43946  jm2.24nn  43965  jm2.17a  43966  jm2.17b  43967  jm2.17c  43968  jm2.18  43994  jm2.19lem2  43996  jm2.22  44001  jm2.23  44002  areaquad  44217  imo72b2  45171  int-mulcomd  45175  int-rightdistd  45179  cvgdvgrat  45296  radcnvrat  45297  bccm1k  45325  binomcxplemwb  45331  binomcxplemnotnn0  45339  sineq0ALT  45918  mul13d  46295  divdiv3d  46370  mccllem  46608  coskpi2  46875  cosknegpi  46878  dvsinax  46922  dvasinbx  46929  dvcosax  46935  dvnxpaek  46951  dvnmul  46952  dvnprodlem2  46956  itgsinexplem1  46963  stoweidlem1  47010  stoweidlem11  47020  stoweidlem26  47035  stoweidlem32  47041  wallispilem4  47077  wallispi2lem1  47080  wallispi2lem2  47081  stirlinglem3  47085  stirlinglem4  47086  stirlinglem5  47087  stirlinglem7  47089  stirlinglem10  47092  stirlinglem15  47097  dirkertrigeqlem1  47107  dirkertrigeqlem2  47108  dirkertrigeqlem3  47109  dirkertrigeq  47110  dirkercncflem1  47112  fourierdlem16  47132  fourierdlem21  47137  fourierdlem22  47138  fourierdlem56  47171  fourierdlem66  47181  fourierdlem83  47198  fourierswlem  47239  fouriersw  47240  etransclem23  47266  etransclem24  47267  etransclem38  47281  etransclem46  47289  hoiprodp1  47597  hoidmvlelem2  47605  smfmullem1  47800  sigarac  47861  sigarls  47866  sigarid  47867  sigardiv  47870  sigarcol  47873  sigaradd  47875  cevathlem1  47876  sin3t  47916  cos3t  47917  sin5tlem1  47918  sin5tlem3  47920  sqrtnegnre  48376  fmtnoodd  48617  sqrtpwpw2p  48622  fmtnorec3  48632  fmtnoprmfac2lem1  48650  fmtnofac1  48654  lighneallem2  48690  lighneallem3  48691  proththd  48698  requad01  48718  dfeven2  48746  fppr2odd  48828  fpprwppr  48836  altgsumbc  49463  altgsumbcALT  49464  blennnt2  49700  dignn0flhalflem2  49727  dignn0ehalf  49728  itcovalt2lem2lem2  49785  affinecomb2  49814  rrx2linest  49853  itscnhlc0yqe  49870  itsclc0yqsollem1  49873  itscnhlc0xyqsol  49876  itschlc0xyqsol1  49877  itsclc0xyqsolr  49880  itsclquadb  49887  2itscplem3  49891  itscnhlinecirc02plem1  49893  itscnhlinecirc02plem2  49894  inlinecirc02p  49898  crosspaltd  50965  crossp3d  50966  amgmwlem  50986