Theorem mulcomd 11125

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  (class class class)co 7341  ℂcc 10996   · cmul 11003

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

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

This theorem is referenced by:  mul31  11272  mul4r  11274  mulcand  11742  mulcan2d  11743  divcan1  11777  divrec2  11785  div23  11787  divdivdiv  11814  divmuleq  11818  divadddiv  11828  divcan5rd  11916  dmdcan2d  11919  mvllmuld  11945  rdiv  11948  subhalfhalf  12347  mul2lt0llt0  12988  mul2lt0lgt0  12989  prodge0ld  12992  xmulcom  13157  modvalr  13768  mulp1mod1  13810  modmul12d  13824  modnegd  13825  modmulmodr  13836  expaddz  14005  binom3  14123  expmulnbnd  14134  digit1  14136  bccmpl  14208  bcm1k  14214  bcn2  14218  bcpasc  14220  recval  15222  abs1m  15235  bhmafibid1cn  15365  bhmafibid2cn  15366  reccn2  15496  lo1mul2  15528  isummulc1  15662  fsummulc1  15684  incexclem  15735  incexc  15736  trireciplem  15761  pwdif  15767  geolim  15769  cvgrat  15782  mertens  15785  ntrivcvgmul  15801  fallfacfwd  15935  bpoly4  15958  fsumcube  15959  eftlub  16010  sinadd  16065  cosadd  16066  sin2t  16078  nndivides  16165  dvds2ln  16192  even2n  16245  oddm1even  16246  mod2eq1n2dvds  16250  m1exp1  16279  pwp1fsum  16294  divalgmod  16309  bitsp1  16334  bitsinv1lem  16344  sadadd2lem  16362  smumullem  16395  gcdmultiplez  16438  mulgcdr  16453  rplpwr  16461  lcmgcdlem  16509  divgcdcoprmex  16569  cncongr1  16570  eulerthlem2  16685  prmdiv  16688  prmdivdiv  16690  vfermltlALT  16706  modprmn0modprm0  16711  coprimeprodsq  16712  pythagtriplem6  16725  pythagtriplem7  16726  pceulem  16749  pcadd  16793  prmpwdvds  16808  mul4sqlem  16857  4sqlem17  16865  mulgassr  19017  odmodnn0  19445  odmulg  19461  odmulgeq  19462  odbezout  19463  odadd1  19753  ablfacrp2  19974  pgpfac1lem3  19984  zringlpirlem3  21394  znunit  21493  icopnfhmeo  24861  cphassr  25132  pjthlem1  25357  itgabs  25756  dvmulbr  25861  dvmulbrOLD  25862  dvcmul  25867  dvcmulf  25868  dvmptcmul  25888  cmvth  25915  cmvthOLD  25916  dvlipcn  25919  c1liplem1  25921  lhop1lem  25938  lhop2  25940  dvcvx  25945  dvfsumlem2  25953  dvfsumlem2OLD  25954  ftc1lem4  25966  itgparts  25974  dvply1  26211  elqaalem3  26249  aalioulem4  26263  taylthlem2  26302  taylthlem2OLD  26303  abelthlem6  26366  abelthlem7  26368  tangtx  26434  tanarg  26548  advlogexp  26584  mulcxp  26614  cxpmul  26617  abscxp  26621  dvcxp2  26670  cxpeq  26687  ang180lem1  26739  lawcoslem1  26745  lawcos  26746  heron  26768  dcubic1  26775  mcubic  26777  cubic2  26778  binom4  26780  dquart  26783  quart1lem  26785  quart1  26786  quartlem1  26787  dvatan  26865  leibpi  26872  log2cnv  26874  efrlim  26899  efrlimOLD  26900  cxp2lim  26907  cxploglim  26908  zetacvg  26945  lgamgulmlem2  26960  lgamgulmlem3  26961  wilthlem1  26998  ftalem1  27003  ftalem5  27007  basellem3  27013  basellem5  27015  mpodvdsmulf1o  27124  dvdsmulf1o  27126  sgmppw  27128  logfac2  27148  chpval2  27149  chpchtsum  27150  perfect1  27159  lgsdirprm  27262  lgsdi  27265  lgsdirnn0  27275  lgsdinn0  27276  gausslemma2dlem1a  27296  gausslemma2dlem6  27303  lgsquadlem1  27311  lgsquadlem2  27312  lgsquadlem3  27313  lgsquad2  27317  2lgslem3a1  27331  2lgslem3b1  27332  2lgslem3c1  27333  2lgslem3d1  27334  2lgsoddprmlem2  27340  2sqlem3  27351  2sqlem4  27352  2sqmod  27367  chebbnd1lem2  27401  chebbnd1lem3  27402  chtppilimlem2  27405  chto1lb  27409  rplogsumlem1  27415  dchrisumlem2  27421  dchrvmasum2lem  27427  dchrisum0flblem2  27440  dchrisum0lem2a  27448  mulogsumlem  27462  mulog2sumlem2  27466  selberglem1  27476  selberg2lem  27481  selberg3lem1  27488  selberg4  27492  pntrsumo1  27496  selberg34r  27502  pntrlog2bndlem3  27510  pntrlog2bndlem4  27511  pntlemb  27528  pntlemq  27532  pntlemr  27533  pntlemj  27534  pntlemo  27538  pnt2  27544  pnt  27545  padicabvcxp  27563  ostth2lem2  27565  ostth2lem3  27566  ostth2lem4  27567  ttgcontlem1  28856  brbtwn2  28876  colinearalglem1  28877  colinearalg  28881  axpaschlem  28911  axcontlem8  28942  numclwwlk1  30331  numclwwlk7  30361  smcnlem  30667  pjhthlem1  31361  kbmul  31925  kbass2  32087  submuladdd  32713  muldivdid  32714  pythagreim  32719  quad3d  32723  sgnmul  32808  2exple2exp  32818  psgnfzto1st  33064  zringfrac  33509  ccfldextdgrr  33675  fldext2rspun  33685  fldext2chn  33731  constrrtlc1  33735  constrrtcclem  33737  constrrtcc  33738  constrremulcl  33770  constrmulcl  33774  cos9thpiminplylem1  33785  qqhval2lem  33984  qqhghm  33991  qqhrhm  33992  oddpwdc  34357  plymulx0  34550  signsvtp  34586  signsvtn  34587  signsvfpn  34588  signsvfnn  34589  breprexplemc  34635  circlemethhgt  34646  logdivsqrle  34653  hgt750lemf  34656  hgt750lemb  34659  hgt750leme  34661  subfacval2  35199  subfaclim  35200  fwddifnp1  36178  knoppndvlem11  36535  knoppndvlem17  36541  bj-subcom  37321  bj-bary1lem1  37324  itg2addnclem  37690  itg2addnclem2  37691  itgabsnc  37708  ftc1cnnclem  37710  areacirclem1  37727  areacirc  37732  geomcau  37778  bfplem1  37841  rrndstprj2  37850  rrnequiv  37854  lcmineqlem1  42041  lcmineqlem5  42045  lcmineqlem8  42048  lcmineqlem11  42051  lcmineqlem18  42058  lcmineqlem21  42061  3lexlogpow5ineq2  42067  3lexlogpow2ineq1  42070  dvrelogpow2b  42080  aks4d1p1p7  42086  primrootscoprmpow  42111  primrootscoprbij  42114  aks6d1c1  42128  aks6d1c2  42142  2np3bcnp1  42156  2ap1caineq  42157  bcle2d  42191  aks6d1c7lem1  42192  nicomachus  42324  retire  42331  readvrec  42374  3cubeslem2  42697  3cubeslem3l  42698  3cubeslem3r  42699  irrapxlem5  42838  pellexlem2  42842  pellexlem6  42846  qirropth  42920  rmxyadd  42933  rmxm1  42946  rmxluc  42948  rmyluc2  42950  rmydbl  42952  jm2.24nn  42971  jm2.17a  42972  jm2.17b  42973  jm2.17c  42974  jm2.18  43000  jm2.19lem2  43002  jm2.22  43007  jm2.23  43008  areaquad  43228  imo72b2  44184  int-mulcomd  44188  int-rightdistd  44192  cvgdvgrat  44325  radcnvrat  44326  bccm1k  44354  binomcxplemwb  44360  binomcxplemnotnn0  44368  sineq0ALT  44948  mul13d  45300  divdiv3d  45377  mccllem  45616  coskpi2  45883  cosknegpi  45886  dvsinax  45930  dvasinbx  45937  dvcosax  45943  dvnxpaek  45959  dvnmul  45960  dvnprodlem2  45964  itgsinexplem1  45971  stoweidlem1  46018  stoweidlem11  46028  stoweidlem26  46043  stoweidlem32  46049  wallispilem4  46085  wallispi2lem1  46088  wallispi2lem2  46089  stirlinglem3  46093  stirlinglem4  46094  stirlinglem5  46095  stirlinglem7  46097  stirlinglem10  46100  stirlinglem15  46105  dirkertrigeqlem1  46115  dirkertrigeqlem2  46116  dirkertrigeqlem3  46117  dirkertrigeq  46118  dirkercncflem1  46120  fourierdlem16  46140  fourierdlem21  46145  fourierdlem22  46146  fourierdlem56  46179  fourierdlem66  46189  fourierdlem83  46206  fourierswlem  46247  fouriersw  46248  etransclem23  46274  etransclem24  46275  etransclem38  46289  etransclem46  46297  hoiprodp1  46605  hoidmvlelem2  46613  smfmullem1  46808  sigarac  46869  sigarls  46874  sigarid  46875  sigardiv  46878  sigarcol  46881  sigaradd  46883  cevathlem1  46884  sqrtnegnre  47317  fmtnoodd  47543  sqrtpwpw2p  47548  fmtnorec3  47558  fmtnoprmfac2lem1  47576  fmtnofac1  47580  lighneallem2  47616  lighneallem3  47617  proththd  47624  requad01  47631  dfeven2  47659  fppr2odd  47741  fpprwppr  47749  altgsumbc  48362  altgsumbcALT  48363  blennnt2  48600  dignn0flhalflem2  48627  dignn0ehalf  48628  itcovalt2lem2lem2  48685  affinecomb2  48714  rrx2linest  48753  itscnhlc0yqe  48770  itsclc0yqsollem1  48773  itscnhlc0xyqsol  48776  itschlc0xyqsol1  48777  itsclc0xyqsolr  48780  itsclquadb  48787  2itscplem3  48791  itscnhlinecirc02plem1  48793  itscnhlinecirc02plem2  48794  inlinecirc02p  48798  amgmwlem  49813