Theorem mulcomd 11193

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

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  (class class class)co 7385  ℂcc 11061   · cmul 11068

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mul31  11340  mul4r  11342  mulcand  11810  mulcan2d  11811  divcan1  11844  divrec2  11852  div23  11854  muldivdid  11875  divdivdiv  11882  divmuleq  11886  divadddiv  11896  divcan5rd  11984  dmdcan2d  11987  mvllmuld  12013  rdiv  12016  subhalfhalf  12445  mul2lt0llt0  13089  mul2lt0lgt0  13090  prodge0ld  13093  xmulcom  13259  modvalr  13872  mulp1mod1  13914  modmul12d  13928  modnegd  13929  modmulmodr  13940  expaddz  14109  binom3  14227  expmulnbnd  14238  digit1  14240  bccmpl  14312  bcm1k  14318  bcn2  14322  bcpasc  14324  recval  15326  abs1m  15339  bhmafibid1cn  15469  bhmafibid2cn  15470  reccn2  15600  lo1mul2  15632  isummulc1  15766  fsummulc1  15788  incexclem  15842  incexc  15843  trireciplem  15868  pwdif  15874  geolim  15876  cvgrat  15889  mertens  15892  ntrivcvgmul  15908  fallfacfwd  16042  bpoly4  16065  fsumcube  16066  eftlub  16117  sinadd  16172  cosadd  16173  sin2t  16185  nndivides  16272  dvds2ln  16299  even2n  16352  oddm1even  16353  mod2eq1n2dvds  16357  m1exp1  16386  pwp1fsum  16401  divalgmod  16416  bitsp1  16441  bitsinv1lem  16451  sadadd2lem  16469  smumullem  16502  gcdmultiplez  16545  mulgcdr  16560  rplpwr  16568  lcmgcdlem  16616  divgcdcoprmex  16676  cncongr1  16677  eulerthlem2  16793  prmdiv  16796  prmdivdiv  16798  vfermltlALT  16814  modprmn0modprm0  16819  coprimeprodsq  16820  pythagtriplem6  16833  pythagtriplem7  16834  pceulem  16857  pcadd  16901  prmpwdvds  16916  mul4sqlem  16965  4sqlem17  16973  mulgassr  19130  odmodnn0  19556  odmulg  19572  odmulgeq  19573  odbezout  19574  odadd1  19864  ablfacrp2  20085  pgpfac1lem3  20095  zringlpirlem3  21489  znunit  21588  icopnfhmeo  24978  cphassr  25247  pjthlem1  25472  itgabs  25870  dvmulbr  25974  dvcmul  25979  dvcmulf  25980  dvmptcmul  25999  cmvth  26026  dvlipcn  26029  c1liplem1  26031  lhop1lem  26048  lhop2  26050  dvcvx  26055  dvfsumlem2  26062  ftc1lem4  26074  itgparts  26082  dvply1  26318  elqaalem3  26355  aalioulem4  26369  taylthlem2  26407  abelthlem6  26469  abelthlem7  26471  tangtx  26540  tanarg  26654  advlogexp  26690  mulcxp  26720  cxpmul  26723  abscxp  26727  dvcxp2  26776  cxpeq  26792  ang180lem1  26844  lawcoslem1  26850  lawcos  26851  heron  26873  dcubic1  26880  mcubic  26882  cubic2  26883  binom4  26885  dquart  26888  quart1lem  26890  quart1  26891  quartlem1  26892  dvatan  26970  leibpi  26977  log2cnv  26979  efrlim  27004  cxp2lim  27011  cxploglim  27012  zetacvg  27049  lgamgulmlem2  27064  lgamgulmlem3  27065  wilthlem1  27102  ftalem1  27107  ftalem5  27111  basellem3  27117  basellem5  27119  mpodvdsmulf1o  27228  dvdsmulf1o  27230  sgmppw  27231  logfac2  27251  chpval2  27252  chpchtsum  27253  perfect1  27262  lgsdirprm  27365  lgsdi  27368  lgsdirnn0  27378  lgsdinn0  27379  gausslemma2dlem1a  27399  gausslemma2dlem6  27406  lgsquadlem1  27414  lgsquadlem2  27415  lgsquadlem3  27416  lgsquad2  27420  2lgslem3a1  27434  2lgslem3b1  27435  2lgslem3c1  27436  2lgslem3d1  27437  2lgsoddprmlem2  27443  2sqlem3  27454  2sqlem4  27455  2sqmod  27470  chebbnd1lem2  27504  chebbnd1lem3  27505  chtppilimlem2  27508  chto1lb  27512  rplogsumlem1  27518  dchrisumlem2  27524  dchrvmasum2lem  27530  dchrisum0flblem2  27543  dchrisum0lem2a  27551  mulogsumlem  27565  mulog2sumlem2  27569  selberglem1  27579  selberg2lem  27584  selberg3lem1  27591  selberg4  27595  pntrsumo1  27599  selberg34r  27605  pntrlog2bndlem3  27613  pntrlog2bndlem4  27614  pntlemb  27631  pntlemq  27635  pntlemr  27636  pntlemj  27637  pntlemo  27641  pnt2  27647  pnt  27648  padicabvcxp  27666  ostth2lem2  27668  ostth2lem3  27669  ostth2lem4  27670  ttgcontlem1  29024  brbtwn2  29045  colinearalglem1  29046  colinearalg  29050  axpaschlem  29080  axcontlem8  29111  numclwwlk1  30502  numclwwlk7  30532  smcnlem  30839  pjhthlem1  31533  kbmul  32097  kbass2  32259  submuladdd  32885  pythagreim  32890  quad3d  32894  sgnmul  32980  2exple2exp  32990  psgnfzto1st  33239  zringfrac  33704  ccfldextdgrr  33923  fldext2rspun  33933  fldext2chn  33979  constrrtlc1  33983  constrrtcclem  33985  constrrtcc  33986  constrremulcl  34018  constrmulcl  34022  cos9thpiminplylem1  34033  qqhval2lem  34232  qqhghm  34239  qqhrhm  34240  oddpwdc  34605  plymulx0  34798  signsvtp  34834  signsvtn  34835  signsvfpn  34836  signsvfnn  34837  breprexplemc  34883  circlemethhgt  34894  logdivsqrle  34901  hgt750lemf  34904  hgt750lemb  34907  hgt750leme  34909  subfacval2  35485  subfaclim  35486  fwddifnp1  36463  knoppndvlem11  36908  knoppndvlem17  36914  bj-subcom  37748  bj-bary1lem1  37751  itg2addnclem  38118  itg2addnclem2  38119  itgabsnc  38136  ftc1cnnclem  38138  areacirclem1  38155  areacirc  38160  geomcau  38206  bfplem1  38269  rrndstprj2  38278  rrnequiv  38282  lcmineqlem1  42594  lcmineqlem5  42598  lcmineqlem8  42601  lcmineqlem11  42604  lcmineqlem18  42611  lcmineqlem21  42614  3lexlogpow5ineq2  42620  3lexlogpow2ineq1  42623  dvrelogpow2b  42633  aks4d1p1p7  42639  primrootscoprmpow  42664  primrootscoprbij  42667  aks6d1c1  42681  aks6d1c2  42695  2np3bcnp1  42709  2ap1caineq  42710  bcle2d  42744  aks6d1c7lem1  42745  nicomachus  42869  retire  42876  readvrec  42919  3cubeslem2  43214  3cubeslem3l  43215  3cubeslem3r  43216  irrapxlem5  43351  pellexlem2  43355  pellexlem6  43359  qirropth  43433  rmxyadd  43446  rmxm1  43459  rmxluc  43461  rmyluc2  43463  rmydbl  43465  jm2.24nn  43484  jm2.17a  43485  jm2.17b  43486  jm2.17c  43487  jm2.18  43513  jm2.19lem2  43515  jm2.22  43520  jm2.23  43521  areaquad  43741  imo72b2  44696  int-mulcomd  44700  int-rightdistd  44704  cvgdvgrat  44837  radcnvrat  44838  bccm1k  44866  binomcxplemwb  44872  binomcxplemnotnn0  44880  sineq0ALT  45460  mul13d  45807  divdiv3d  45883  mccllem  46121  coskpi2  46388  cosknegpi  46391  dvsinax  46435  dvasinbx  46442  dvcosax  46448  dvnxpaek  46464  dvnmul  46465  dvnprodlem2  46469  itgsinexplem1  46476  stoweidlem1  46523  stoweidlem11  46533  stoweidlem26  46548  stoweidlem32  46554  wallispilem4  46590  wallispi2lem1  46593  wallispi2lem2  46594  stirlinglem3  46598  stirlinglem4  46599  stirlinglem5  46600  stirlinglem7  46602  stirlinglem10  46605  stirlinglem15  46610  dirkertrigeqlem1  46620  dirkertrigeqlem2  46621  dirkertrigeqlem3  46622  dirkertrigeq  46623  dirkercncflem1  46625  fourierdlem16  46645  fourierdlem21  46650  fourierdlem22  46651  fourierdlem56  46684  fourierdlem66  46694  fourierdlem83  46711  fourierswlem  46752  fouriersw  46753  etransclem23  46779  etransclem24  46780  etransclem38  46794  etransclem46  46802  hoiprodp1  47110  hoidmvlelem2  47118  smfmullem1  47313  sigarac  47374  sigarls  47379  sigarid  47380  sigardiv  47383  sigarcol  47386  sigaradd  47388  cevathlem1  47389  sin3t  47413  cos3t  47414  sin5tlem1  47415  sin5tlem3  47417  sqrtnegnre  47849  fmtnoodd  48090  sqrtpwpw2p  48095  fmtnorec3  48105  fmtnoprmfac2lem1  48123  fmtnofac1  48127  lighneallem2  48163  lighneallem3  48164  proththd  48171  requad01  48191  dfeven2  48219  fppr2odd  48301  fpprwppr  48309  altgsumbc  48922  altgsumbcALT  48923  blennnt2  49159  dignn0flhalflem2  49186  dignn0ehalf  49187  itcovalt2lem2lem2  49244  affinecomb2  49273  rrx2linest  49312  itscnhlc0yqe  49329  itsclc0yqsollem1  49332  itscnhlc0xyqsol  49335  itschlc0xyqsol1  49336  itsclc0xyqsolr  49339  itsclquadb  49346  2itscplem3  49350  itscnhlinecirc02plem1  49352  itscnhlinecirc02plem2  49353  inlinecirc02p  49357  amgmwlem  50371