Theorem mulcomd 11143

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11014   · cmul 11021

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

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

This theorem is referenced by:  mul31  11290  mul4r  11292  mulcand  11760  mulcan2d  11761  divcan1  11795  divrec2  11803  div23  11805  divdivdiv  11832  divmuleq  11836  divadddiv  11846  divcan5rd  11934  dmdcan2d  11937  mvllmuld  11963  rdiv  11966  subhalfhalf  12365  mul2lt0llt0  13006  mul2lt0lgt0  13007  prodge0ld  13010  xmulcom  13175  modvalr  13786  mulp1mod1  13828  modmul12d  13842  modnegd  13843  modmulmodr  13854  expaddz  14023  binom3  14141  expmulnbnd  14152  digit1  14154  bccmpl  14226  bcm1k  14232  bcn2  14236  bcpasc  14238  recval  15240  abs1m  15253  bhmafibid1cn  15383  bhmafibid2cn  15384  reccn2  15514  lo1mul2  15546  isummulc1  15680  fsummulc1  15702  incexclem  15753  incexc  15754  trireciplem  15779  pwdif  15785  geolim  15787  cvgrat  15800  mertens  15803  ntrivcvgmul  15819  fallfacfwd  15953  bpoly4  15976  fsumcube  15977  eftlub  16028  sinadd  16083  cosadd  16084  sin2t  16096  nndivides  16183  dvds2ln  16210  even2n  16263  oddm1even  16264  mod2eq1n2dvds  16268  m1exp1  16297  pwp1fsum  16312  divalgmod  16327  bitsp1  16352  bitsinv1lem  16362  sadadd2lem  16380  smumullem  16413  gcdmultiplez  16456  mulgcdr  16471  rplpwr  16479  lcmgcdlem  16527  divgcdcoprmex  16587  cncongr1  16588  eulerthlem2  16703  prmdiv  16706  prmdivdiv  16708  vfermltlALT  16724  modprmn0modprm0  16729  coprimeprodsq  16730  pythagtriplem6  16743  pythagtriplem7  16744  pceulem  16767  pcadd  16811  prmpwdvds  16826  mul4sqlem  16875  4sqlem17  16883  mulgassr  19035  odmodnn0  19462  odmulg  19478  odmulgeq  19479  odbezout  19480  odadd1  19770  ablfacrp2  19991  pgpfac1lem3  20001  zringlpirlem3  21411  znunit  21510  icopnfhmeo  24878  cphassr  25149  pjthlem1  25374  itgabs  25773  dvmulbr  25878  dvmulbrOLD  25879  dvcmul  25884  dvcmulf  25885  dvmptcmul  25905  cmvth  25932  cmvthOLD  25933  dvlipcn  25936  c1liplem1  25938  lhop1lem  25955  lhop2  25957  dvcvx  25962  dvfsumlem2  25970  dvfsumlem2OLD  25971  ftc1lem4  25983  itgparts  25991  dvply1  26228  elqaalem3  26266  aalioulem4  26280  taylthlem2  26319  taylthlem2OLD  26320  abelthlem6  26383  abelthlem7  26385  tangtx  26451  tanarg  26565  advlogexp  26601  mulcxp  26631  cxpmul  26634  abscxp  26638  dvcxp2  26687  cxpeq  26704  ang180lem1  26756  lawcoslem1  26762  lawcos  26763  heron  26785  dcubic1  26792  mcubic  26794  cubic2  26795  binom4  26797  dquart  26800  quart1lem  26802  quart1  26803  quartlem1  26804  dvatan  26882  leibpi  26889  log2cnv  26891  efrlim  26916  efrlimOLD  26917  cxp2lim  26924  cxploglim  26925  zetacvg  26962  lgamgulmlem2  26977  lgamgulmlem3  26978  wilthlem1  27015  ftalem1  27020  ftalem5  27024  basellem3  27030  basellem5  27032  mpodvdsmulf1o  27141  dvdsmulf1o  27143  sgmppw  27145  logfac2  27165  chpval2  27166  chpchtsum  27167  perfect1  27176  lgsdirprm  27279  lgsdi  27282  lgsdirnn0  27292  lgsdinn0  27293  gausslemma2dlem1a  27313  gausslemma2dlem6  27320  lgsquadlem1  27328  lgsquadlem2  27329  lgsquadlem3  27330  lgsquad2  27334  2lgslem3a1  27348  2lgslem3b1  27349  2lgslem3c1  27350  2lgslem3d1  27351  2lgsoddprmlem2  27357  2sqlem3  27368  2sqlem4  27369  2sqmod  27384  chebbnd1lem2  27418  chebbnd1lem3  27419  chtppilimlem2  27422  chto1lb  27426  rplogsumlem1  27432  dchrisumlem2  27438  dchrvmasum2lem  27444  dchrisum0flblem2  27457  dchrisum0lem2a  27465  mulogsumlem  27479  mulog2sumlem2  27483  selberglem1  27493  selberg2lem  27498  selberg3lem1  27505  selberg4  27509  pntrsumo1  27513  selberg34r  27519  pntrlog2bndlem3  27527  pntrlog2bndlem4  27528  pntlemb  27545  pntlemq  27549  pntlemr  27550  pntlemj  27551  pntlemo  27555  pnt2  27561  pnt  27562  padicabvcxp  27580  ostth2lem2  27582  ostth2lem3  27583  ostth2lem4  27584  ttgcontlem1  28873  brbtwn2  28894  colinearalglem1  28895  colinearalg  28899  axpaschlem  28929  axcontlem8  28960  numclwwlk1  30352  numclwwlk7  30382  smcnlem  30688  pjhthlem1  31382  kbmul  31946  kbass2  32108  submuladdd  32734  muldivdid  32735  pythagreim  32740  quad3d  32744  sgnmul  32829  2exple2exp  32839  psgnfzto1st  33085  zringfrac  33530  ccfldextdgrr  33696  fldext2rspun  33706  fldext2chn  33752  constrrtlc1  33756  constrrtcclem  33758  constrrtcc  33759  constrremulcl  33791  constrmulcl  33795  cos9thpiminplylem1  33806  qqhval2lem  34005  qqhghm  34012  qqhrhm  34013  oddpwdc  34378  plymulx0  34571  signsvtp  34607  signsvtn  34608  signsvfpn  34609  signsvfnn  34610  breprexplemc  34656  circlemethhgt  34667  logdivsqrle  34674  hgt750lemf  34677  hgt750lemb  34680  hgt750leme  34682  subfacval2  35242  subfaclim  35243  fwddifnp1  36220  knoppndvlem11  36577  knoppndvlem17  36583  bj-subcom  37363  bj-bary1lem1  37366  itg2addnclem  37721  itg2addnclem2  37722  itgabsnc  37739  ftc1cnnclem  37741  areacirclem1  37758  areacirc  37763  geomcau  37809  bfplem1  37872  rrndstprj2  37881  rrnequiv  37885  lcmineqlem1  42132  lcmineqlem5  42136  lcmineqlem8  42139  lcmineqlem11  42142  lcmineqlem18  42149  lcmineqlem21  42152  3lexlogpow5ineq2  42158  3lexlogpow2ineq1  42161  dvrelogpow2b  42171  aks4d1p1p7  42177  primrootscoprmpow  42202  primrootscoprbij  42205  aks6d1c1  42219  aks6d1c2  42233  2np3bcnp1  42247  2ap1caineq  42248  bcle2d  42282  aks6d1c7lem1  42283  nicomachus  42420  retire  42427  readvrec  42470  3cubeslem2  42792  3cubeslem3l  42793  3cubeslem3r  42794  irrapxlem5  42933  pellexlem2  42937  pellexlem6  42941  qirropth  43015  rmxyadd  43028  rmxm1  43041  rmxluc  43043  rmyluc2  43045  rmydbl  43047  jm2.24nn  43066  jm2.17a  43067  jm2.17b  43068  jm2.17c  43069  jm2.18  43095  jm2.19lem2  43097  jm2.22  43102  jm2.23  43103  areaquad  43323  imo72b2  44279  int-mulcomd  44283  int-rightdistd  44287  cvgdvgrat  44420  radcnvrat  44421  bccm1k  44449  binomcxplemwb  44455  binomcxplemnotnn0  44463  sineq0ALT  45043  mul13d  45395  divdiv3d  45472  mccllem  45711  coskpi2  45978  cosknegpi  45981  dvsinax  46025  dvasinbx  46032  dvcosax  46038  dvnxpaek  46054  dvnmul  46055  dvnprodlem2  46059  itgsinexplem1  46066  stoweidlem1  46113  stoweidlem11  46123  stoweidlem26  46138  stoweidlem32  46144  wallispilem4  46180  wallispi2lem1  46183  wallispi2lem2  46184  stirlinglem3  46188  stirlinglem4  46189  stirlinglem5  46190  stirlinglem7  46192  stirlinglem10  46195  stirlinglem15  46200  dirkertrigeqlem1  46210  dirkertrigeqlem2  46211  dirkertrigeqlem3  46212  dirkertrigeq  46213  dirkercncflem1  46215  fourierdlem16  46235  fourierdlem21  46240  fourierdlem22  46241  fourierdlem56  46274  fourierdlem66  46284  fourierdlem83  46301  fourierswlem  46342  fouriersw  46343  etransclem23  46369  etransclem24  46370  etransclem38  46384  etransclem46  46392  hoiprodp1  46700  hoidmvlelem2  46708  smfmullem1  46903  sigarac  46964  sigarls  46969  sigarid  46970  sigardiv  46973  sigarcol  46976  sigaradd  46978  cevathlem1  46979  sqrtnegnre  47421  fmtnoodd  47647  sqrtpwpw2p  47652  fmtnorec3  47662  fmtnoprmfac2lem1  47680  fmtnofac1  47684  lighneallem2  47720  lighneallem3  47721  proththd  47728  requad01  47735  dfeven2  47763  fppr2odd  47845  fpprwppr  47853  altgsumbc  48466  altgsumbcALT  48467  blennnt2  48704  dignn0flhalflem2  48731  dignn0ehalf  48732  itcovalt2lem2lem2  48789  affinecomb2  48818  rrx2linest  48857  itscnhlc0yqe  48874  itsclc0yqsollem1  48877  itscnhlc0xyqsol  48880  itschlc0xyqsol1  48881  itsclc0xyqsolr  48884  itsclquadb  48891  2itscplem3  48895  itscnhlinecirc02plem1  48897  itscnhlinecirc02plem2  48898  inlinecirc02p  48902  amgmwlem  49917