Theorem mulcomd 11236

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  (class class class)co 7412  ℂcc 11104   · cmul 11111

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

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

This theorem is used by:  mul31  11383  mul4r  11385  mulcand  11853  mulcan2d  11854  divcan1  11887  divrec2  11895  div23  11897  muldivdid  11915  divdivdiv  11922  divmuleq  11926  divadddiv  11936  divcan5rd  12024  dmdcan2d  12027  mvllmuld  12053  rdiv  12056  subhalfhalf  12484  mul2lt0llt0  13128  mul2lt0lgt0  13129  prodge0ld  13132  xmulcom  13298  modvalr  13912  mulp1mod1  13954  modmul12d  13968  modnegd  13969  modmulmodr  13980  expaddz  14149  binom3  14267  expmulnbnd  14278  digit1  14280  bccmpl  14352  bcm1k  14358  bcn2  14362  bcpasc  14364  sgnmul  15151  recval  15381  abs1m  15394  bhmafibid1cn  15524  bhmafibid2cn  15525  reccn2  15655  lo1mul2  15687  isummulc1  15821  fsummulc1  15843  incexclem  15897  incexc  15898  trireciplem  15923  pwdif  15929  geolim  15931  cvgrat  15944  mertens  15947  ntrivcvgmul  15963  fallfacfwd  16096  bpoly4  16119  fsumcube  16120  eftlub  16171  sinadd  16226  cosadd  16227  sin2t  16239  nndivides  16326  dvds2ln  16353  even2n  16406  oddm1even  16407  mod2eq1n2dvds  16411  m1exp1  16440  pwp1fsum  16455  divalgmod  16470  bitsp1  16495  bitsinv1lem  16505  sadadd2lem  16523  smumullem  16556  gcdmultiplez  16599  mulgcdr  16614  rplpwr  16622  lcmgcdlem  16670  divgcdcoprmex  16730  cncongr1  16731  eulerthlem2  16847  prmdiv  16850  prmdivdiv  16852  vfermltlALT  16868  modprmn0modprm0  16873  coprimeprodsq  16874  pythagtriplem6  16887  pythagtriplem7  16888  pceulem  16911  pcadd  16955  prmpwdvds  16970  mul4sqlem  17019  4sqlem17  17027  mulgassr  19184  odmodnn0  19616  odmulg  19632  odmulgeq  19633  odbezout  19634  odadd1  19924  ablfacrp2  20145  pgpfac1lem3  20155  zringlpirlem3  21625  znunit  21724  icopnfhmeo  25113  cphassr  25382  pjthlem1  25607  itgabs  26005  dvmulbr  26109  dvcmul  26114  dvcmulf  26115  dvmptcmul  26134  cmvth  26161  dvlipcn  26164  c1liplem1  26166  lhop1lem  26183  lhop2  26185  dvcvx  26190  dvfsumlem2  26197  ftc1lem4  26209  itgparts  26217  plyn0mulidp  26453  dvply1  26456  elqaalem3  26493  aalioulem4  26509  taylthlem2  26548  abelthlem6  26610  abelthlem7  26612  tangtx  26681  tanarg  26795  advlogexp  26831  mulcxp  26861  cxpmul  26864  abscxp  26868  dvcxp2  26917  cxpeq  26933  ang180lem1  26985  lawcoslem1  26991  lawcos  26992  heron  27014  dcubic1  27021  mcubic  27023  cubic2  27024  binom4  27026  dquart  27029  quart1lem  27031  quart1  27032  quartlem1  27033  dvatan  27111  leibpi  27118  log2cnv  27120  efrlim  27145  cxp2lim  27152  cxploglim  27153  zetacvg  27190  lgamgulmlem2  27205  lgamgulmlem3  27206  wilthlem1  27243  ftalem1  27248  ftalem5  27252  basellem3  27258  basellem5  27260  basellem8  27263  mpodvdsmulf1o  27369  dvdsmulf1o  27371  sgmppw  27372  logfac2  27392  chpval2  27393  chpchtsum  27394  perfect1  27403  lgsdirprm  27506  lgsdi  27509  lgsdirnn0  27519  lgsdinn0  27520  gausslemma2dlem1a  27540  gausslemma2dlem6  27547  lgsquadlem1  27555  lgsquadlem2  27556  lgsquadlem3  27557  lgsquad2  27561  2lgslem3a1  27575  2lgslem3b1  27576  2lgslem3c1  27577  2lgslem3d1  27578  2lgsoddprmlem2  27584  2sqlem3  27595  2sqlem4  27596  2sqmod  27611  chebbnd1lem2  27645  chebbnd1lem3  27646  chtppilimlem2  27649  chto1lb  27653  rplogsumlem1  27659  dchrisumlem2  27665  dchrvmasum2lem  27671  dchrisum0flblem2  27684  dchrisum0lem2a  27692  mulogsumlem  27706  mulog2sumlem2  27710  selberglem1  27720  selberg2lem  27725  selberg3lem1  27732  selberg4  27736  pntrsumo1  27740  selberg34r  27746  pntrlog2bndlem3  27754  pntrlog2bndlem4  27755  pntlemb  27772  pntlemq  27776  pntlemr  27777  pntlemj  27778  pntlemo  27782  pnt2  27788  pnt  27789  padicabvcxp  27807  ostth2lem2  27809  ostth2lem3  27810  ostth2lem4  27811  ttgcontlem1  29245  brbtwn2  29266  colinearalglem1  29267  colinearalg  29271  axpaschlem  29301  axcontlem8  29332  numclwwlk1  30723  numclwwlk7  30753  smcnlem  31060  pjhthlem1  31754  kbmul  32318  kbass2  32480  submuladdd  33096  pythagreim  33101  quad3d  33105  2exple2exp  33189  psgnfzto1st  33434  zringfrac  33853  ccfldextdgrr  34071  fldext2rspun  34081  fldext2chn  34127  constrrtlc1  34131  constrrtcclem  34133  constrrtcc  34134  constrremulcl  34166  constrmulcl  34170  cos9thpiminplylem1  34181  qqhval2lem  34380  qqhghm  34387  qqhrhm  34388  oddpwdc  34753  signsvtp  34979  signsvtn  34980  signsvfpn  34981  signsvfnn  34982  breprexplemc  35028  circlemethhgt  35039  logdivsqrle  35046  hgt750lemf  35049  hgt750lemb  35052  hgt750leme  35054  subfacval2  35687  subfaclim  35688  fwddifnp1  36665  knoppndvlem11  37139  knoppndvlem17  37145  bj-subcom  37980  bj-bary1lem1  37983  itg2addnclem  38350  itg2addnclem2  38351  itgabsnc  38368  ftc1cnnclem  38370  areacirclem1  38387  areacirc  38392  geomcau  38438  bfplem1  38501  rrndstprj2  38510  rrnequiv  38514  lcmineqlem1  42824  lcmineqlem5  42828  lcmineqlem8  42831  lcmineqlem11  42834  lcmineqlem18  42841  lcmineqlem21  42844  3lexlogpow5ineq2  42850  3lexlogpow2ineq1  42853  dvrelogpow2b  42863  aks4d1p1p7  42869  primrootscoprmpow  42894  primrootscoprbij  42897  aks6d1c1  42911  aks6d1c2  42925  2np3bcnp1  42939  2ap1caineq  42940  bcle2d  42974  aks6d1c7lem1  42975  quadfac  43000  nicomachus  43101  retire  43108  readvrec  43151  3cubeslem2  43444  3cubeslem3l  43445  3cubeslem3r  43446  irrapxlem5  43581  pellexlem2  43585  pellexlem6  43589  qirropth  43663  rmxyadd  43676  rmxm1  43689  rmxluc  43691  rmyluc2  43693  rmydbl  43695  jm2.24nn  43714  jm2.17a  43715  jm2.17b  43716  jm2.17c  43717  jm2.18  43743  jm2.19lem2  43745  jm2.22  43750  jm2.23  43751  areaquad  43971  imo72b2  44926  int-mulcomd  44930  int-rightdistd  44934  cvgdvgrat  45051  radcnvrat  45052  bccm1k  45080  binomcxplemwb  45086  binomcxplemnotnn0  45094  sineq0ALT  45673  mul13d  46027  divdiv3d  46103  mccllem  46341  coskpi2  46608  cosknegpi  46611  dvsinax  46655  dvasinbx  46662  dvcosax  46668  dvnxpaek  46684  dvnmul  46685  dvnprodlem2  46689  itgsinexplem1  46696  stoweidlem1  46743  stoweidlem11  46753  stoweidlem26  46768  stoweidlem32  46774  wallispilem4  46810  wallispi2lem1  46813  wallispi2lem2  46814  stirlinglem3  46818  stirlinglem4  46819  stirlinglem5  46820  stirlinglem7  46822  stirlinglem10  46825  stirlinglem15  46830  dirkertrigeqlem1  46840  dirkertrigeqlem2  46841  dirkertrigeqlem3  46842  dirkertrigeq  46843  dirkercncflem1  46845  fourierdlem16  46865  fourierdlem21  46870  fourierdlem22  46871  fourierdlem56  46904  fourierdlem66  46914  fourierdlem83  46931  fourierswlem  46972  fouriersw  46973  etransclem23  46999  etransclem24  47000  etransclem38  47014  etransclem46  47022  hoiprodp1  47330  hoidmvlelem2  47338  smfmullem1  47533  sigarac  47594  sigarls  47599  sigarid  47600  sigardiv  47603  sigarcol  47606  sigaradd  47608  cevathlem1  47609  sin3t  47636  cos3t  47637  sin5tlem1  47638  sin5tlem3  47640  sqrtnegnre  48072  fmtnoodd  48313  sqrtpwpw2p  48318  fmtnorec3  48328  fmtnoprmfac2lem1  48346  fmtnofac1  48350  lighneallem2  48386  lighneallem3  48387  proththd  48394  requad01  48414  dfeven2  48442  fppr2odd  48524  fpprwppr  48532  altgsumbc  49160  altgsumbcALT  49161  blennnt2  49397  dignn0flhalflem2  49424  dignn0ehalf  49425  itcovalt2lem2lem2  49482  affinecomb2  49511  rrx2linest  49550  itscnhlc0yqe  49567  itsclc0yqsollem1  49570  itscnhlc0xyqsol  49573  itschlc0xyqsol1  49574  itsclc0xyqsolr  49577  itsclquadb  49584  2itscplem3  49588  itscnhlinecirc02plem1  49590  itscnhlinecirc02plem2  49591  inlinecirc02p  49595  crossp3i  50676  amgmwlem  50677