Theorem mulcomd 11279

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   · cmul 11157

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

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

This theorem is referenced by:  mul31  11425  mul4r  11427  mulcand  11893  mulcan2d  11894  divcan1  11928  divrec2  11936  div23  11938  divdivdiv  11965  divmuleq  11969  divadddiv  11979  divcan5rd  12067  dmdcan2d  12070  mvllmuld  12096  rdiv  12099  subhalfhalf  12497  mul2lt0llt0  13136  mul2lt0lgt0  13137  prodge0ld  13140  xmulcom  13304  modvalr  13908  mulp1mod1  13948  modmul12d  13962  modnegd  13963  modmulmodr  13974  expaddz  14143  binom3  14259  expmulnbnd  14270  digit1  14272  bccmpl  14344  bcm1k  14350  bcn2  14354  bcpasc  14356  recval  15357  abs1m  15370  bhmafibid1cn  15498  bhmafibid2cn  15499  reccn2  15629  lo1mul2  15661  isummulc1  15795  fsummulc1  15817  incexclem  15868  incexc  15869  trireciplem  15894  pwdif  15900  geolim  15902  cvgrat  15915  mertens  15918  ntrivcvgmul  15934  fallfacfwd  16068  bpoly4  16091  fsumcube  16092  eftlub  16141  sinadd  16196  cosadd  16197  sin2t  16209  nndivides  16296  dvds2ln  16322  even2n  16375  oddm1even  16376  mod2eq1n2dvds  16380  m1exp1  16409  pwp1fsum  16424  divalgmod  16439  bitsp1  16464  bitsinv1lem  16474  sadadd2lem  16492  smumullem  16525  gcdmultiplez  16568  mulgcdr  16583  rplpwr  16591  lcmgcdlem  16639  divgcdcoprmex  16699  cncongr1  16700  eulerthlem2  16815  prmdiv  16818  prmdivdiv  16820  vfermltlALT  16835  modprmn0modprm0  16840  coprimeprodsq  16841  pythagtriplem6  16854  pythagtriplem7  16855  pceulem  16878  pcadd  16922  prmpwdvds  16937  mul4sqlem  16986  4sqlem17  16994  mulgassr  19142  odmodnn0  19572  odmulg  19588  odmulgeq  19589  odbezout  19590  odadd1  19880  ablfacrp2  20101  pgpfac1lem3  20111  zringlpirlem3  21492  znunit  21599  icopnfhmeo  24987  cphassr  25259  pjthlem1  25484  itgabs  25884  dvmulbr  25989  dvmulbrOLD  25990  dvcmul  25995  dvcmulf  25996  dvmptcmul  26016  cmvth  26043  cmvthOLD  26044  dvlipcn  26047  c1liplem1  26049  lhop1lem  26066  lhop2  26068  dvcvx  26073  dvfsumlem2  26081  dvfsumlem2OLD  26082  ftc1lem4  26094  itgparts  26102  dvply1  26339  elqaalem3  26377  aalioulem4  26391  taylthlem2  26430  taylthlem2OLD  26431  abelthlem6  26494  abelthlem7  26496  tangtx  26561  tanarg  26675  advlogexp  26711  mulcxp  26741  cxpmul  26744  abscxp  26748  dvcxp2  26797  cxpeq  26814  ang180lem1  26866  lawcoslem1  26872  lawcos  26873  heron  26895  dcubic1  26902  mcubic  26904  cubic2  26905  binom4  26907  dquart  26910  quart1lem  26912  quart1  26913  quartlem1  26914  dvatan  26992  leibpi  26999  log2cnv  27001  efrlim  27026  efrlimOLD  27027  cxp2lim  27034  cxploglim  27035  zetacvg  27072  lgamgulmlem2  27087  lgamgulmlem3  27088  wilthlem1  27125  ftalem1  27130  ftalem5  27134  basellem3  27140  basellem5  27142  mpodvdsmulf1o  27251  dvdsmulf1o  27253  sgmppw  27255  logfac2  27275  chpval2  27276  chpchtsum  27277  perfect1  27286  lgsdirprm  27389  lgsdi  27392  lgsdirnn0  27402  lgsdinn0  27403  gausslemma2dlem1a  27423  gausslemma2dlem6  27430  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  lgsquad2  27444  2lgslem3a1  27458  2lgslem3b1  27459  2lgslem3c1  27460  2lgslem3d1  27461  2lgsoddprmlem2  27467  2sqlem3  27478  2sqlem4  27479  2sqmod  27494  chebbnd1lem2  27528  chebbnd1lem3  27529  chtppilimlem2  27532  chto1lb  27536  rplogsumlem1  27542  dchrisumlem2  27548  dchrvmasum2lem  27554  dchrisum0flblem2  27567  dchrisum0lem2a  27575  mulogsumlem  27589  mulog2sumlem2  27593  selberglem1  27603  selberg2lem  27608  selberg3lem1  27615  selberg4  27619  pntrsumo1  27623  selberg34r  27629  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntlemb  27655  pntlemq  27659  pntlemr  27660  pntlemj  27661  pntlemo  27665  pnt2  27671  pnt  27672  padicabvcxp  27690  ostth2lem2  27692  ostth2lem3  27693  ostth2lem4  27694  ttgcontlem1  28913  brbtwn2  28934  colinearalglem1  28935  colinearalg  28939  axpaschlem  28969  axcontlem8  29000  numclwwlk1  30389  numclwwlk7  30419  smcnlem  30725  pjhthlem1  31419  kbmul  31983  kbass2  32145  submuladdd  32756  muldivdid  32757  quad3d  32760  psgnfzto1st  33107  zringfrac  33561  ccfldextdgrr  33696  fldext2chn  33733  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  qqhval2lem  33943  qqhghm  33950  qqhrhm  33951  oddpwdc  34335  sgnmul  34523  plymulx0  34540  signsvtp  34576  signsvtn  34577  signsvfpn  34578  signsvfnn  34579  breprexplemc  34625  circlemethhgt  34636  logdivsqrle  34643  hgt750lemf  34646  hgt750lemb  34649  hgt750leme  34651  subfacval2  35171  subfaclim  35172  fwddifnp1  36146  knoppndvlem11  36504  knoppndvlem17  36510  bj-subcom  37290  bj-bary1lem1  37293  itg2addnclem  37657  itg2addnclem2  37658  itgabsnc  37675  ftc1cnnclem  37677  areacirclem1  37694  areacirc  37699  geomcau  37745  bfplem1  37808  rrndstprj2  37817  rrnequiv  37821  lcmineqlem1  42010  lcmineqlem5  42014  lcmineqlem8  42017  lcmineqlem11  42020  lcmineqlem18  42027  lcmineqlem21  42030  3lexlogpow5ineq2  42036  3lexlogpow2ineq1  42039  dvrelogpow2b  42049  aks4d1p1p7  42055  primrootscoprmpow  42080  primrootscoprbij  42083  aks6d1c1  42097  aks6d1c2  42111  2np3bcnp1  42125  2ap1caineq  42126  bcle2d  42160  aks6d1c7lem1  42161  nicomachus  42324  retire  42332  readvrec  42370  3cubeslem2  42672  3cubeslem3l  42673  3cubeslem3r  42674  irrapxlem5  42813  pellexlem2  42817  pellexlem6  42821  qirropth  42895  rmxyadd  42909  rmxm1  42922  rmxluc  42924  rmyluc2  42926  rmydbl  42928  jm2.24nn  42947  jm2.17a  42948  jm2.17b  42949  jm2.17c  42950  jm2.18  42976  jm2.19lem2  42978  jm2.22  42983  jm2.23  42984  areaquad  43204  imo72b2  44161  int-mulcomd  44165  int-rightdistd  44169  cvgdvgrat  44308  radcnvrat  44309  bccm1k  44337  binomcxplemwb  44343  binomcxplemnotnn0  44351  sineq0ALT  44934  mul13d  45229  divdiv3d  45308  mccllem  45552  coskpi2  45821  cosknegpi  45824  dvsinax  45868  dvasinbx  45875  dvcosax  45881  dvnxpaek  45897  dvnmul  45898  dvnprodlem2  45902  itgsinexplem1  45909  stoweidlem1  45956  stoweidlem11  45966  stoweidlem26  45981  stoweidlem32  45987  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem7  46035  stirlinglem10  46038  stirlinglem15  46043  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem1  46058  fourierdlem16  46078  fourierdlem21  46083  fourierdlem22  46084  fourierdlem56  46117  fourierdlem66  46127  fourierdlem83  46144  fourierswlem  46185  fouriersw  46186  etransclem23  46212  etransclem24  46213  etransclem38  46227  etransclem46  46235  hoiprodp1  46543  hoidmvlelem2  46551  smfmullem1  46746  sigarac  46807  sigarls  46812  sigarid  46813  sigardiv  46816  sigarcol  46819  sigaradd  46821  cevathlem1  46822  sqrtnegnre  47256  fmtnoodd  47457  sqrtpwpw2p  47462  fmtnorec3  47472  fmtnoprmfac2lem1  47490  fmtnofac1  47494  lighneallem2  47530  lighneallem3  47531  proththd  47538  requad01  47545  dfeven2  47573  fppr2odd  47655  fpprwppr  47663  altgsumbc  48196  altgsumbcALT  48197  blennnt2  48438  dignn0flhalflem2  48465  dignn0ehalf  48466  itcovalt2lem2lem2  48523  affinecomb2  48552  rrx2linest  48591  itscnhlc0yqe  48608  itsclc0yqsollem1  48611  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615  itsclc0xyqsolr  48618  itsclquadb  48625  2itscplem3  48629  itscnhlinecirc02plem1  48631  itscnhlinecirc02plem2  48632  inlinecirc02p  48636  amgmwlem  49032