Theorem mulcomd 11153

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

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

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

This theorem is referenced by:  mul31  11300  mul4r  11302  mulcand  11770  mulcan2d  11771  divcan1  11805  divrec2  11813  div23  11815  divdivdiv  11842  divmuleq  11846  divadddiv  11856  divcan5rd  11944  dmdcan2d  11947  mvllmuld  11973  rdiv  11976  subhalfhalf  12375  mul2lt0llt0  13011  mul2lt0lgt0  13012  prodge0ld  13015  xmulcom  13181  modvalr  13792  mulp1mod1  13834  modmul12d  13848  modnegd  13849  modmulmodr  13860  expaddz  14029  binom3  14147  expmulnbnd  14158  digit1  14160  bccmpl  14232  bcm1k  14238  bcn2  14242  bcpasc  14244  recval  15246  abs1m  15259  bhmafibid1cn  15389  bhmafibid2cn  15390  reccn2  15520  lo1mul2  15552  isummulc1  15686  fsummulc1  15708  incexclem  15759  incexc  15760  trireciplem  15785  pwdif  15791  geolim  15793  cvgrat  15806  mertens  15809  ntrivcvgmul  15825  fallfacfwd  15959  bpoly4  15982  fsumcube  15983  eftlub  16034  sinadd  16089  cosadd  16090  sin2t  16102  nndivides  16189  dvds2ln  16216  even2n  16269  oddm1even  16270  mod2eq1n2dvds  16274  m1exp1  16303  pwp1fsum  16318  divalgmod  16333  bitsp1  16358  bitsinv1lem  16368  sadadd2lem  16386  smumullem  16419  gcdmultiplez  16462  mulgcdr  16477  rplpwr  16485  lcmgcdlem  16533  divgcdcoprmex  16593  cncongr1  16594  eulerthlem2  16709  prmdiv  16712  prmdivdiv  16714  vfermltlALT  16730  modprmn0modprm0  16735  coprimeprodsq  16736  pythagtriplem6  16749  pythagtriplem7  16750  pceulem  16773  pcadd  16817  prmpwdvds  16832  mul4sqlem  16881  4sqlem17  16889  mulgassr  19042  odmodnn0  19469  odmulg  19485  odmulgeq  19486  odbezout  19487  odadd1  19777  ablfacrp2  19998  pgpfac1lem3  20008  zringlpirlem3  21419  znunit  21518  icopnfhmeo  24897  cphassr  25168  pjthlem1  25393  itgabs  25792  dvmulbr  25897  dvmulbrOLD  25898  dvcmul  25903  dvcmulf  25904  dvmptcmul  25924  cmvth  25951  cmvthOLD  25952  dvlipcn  25955  c1liplem1  25957  lhop1lem  25974  lhop2  25976  dvcvx  25981  dvfsumlem2  25989  dvfsumlem2OLD  25990  ftc1lem4  26002  itgparts  26010  dvply1  26247  elqaalem3  26285  aalioulem4  26299  taylthlem2  26338  taylthlem2OLD  26339  abelthlem6  26402  abelthlem7  26404  tangtx  26470  tanarg  26584  advlogexp  26620  mulcxp  26650  cxpmul  26653  abscxp  26657  dvcxp2  26706  cxpeq  26723  ang180lem1  26775  lawcoslem1  26781  lawcos  26782  heron  26804  dcubic1  26811  mcubic  26813  cubic2  26814  binom4  26816  dquart  26819  quart1lem  26821  quart1  26822  quartlem1  26823  dvatan  26901  leibpi  26908  log2cnv  26910  efrlim  26935  efrlimOLD  26936  cxp2lim  26943  cxploglim  26944  zetacvg  26981  lgamgulmlem2  26996  lgamgulmlem3  26997  wilthlem1  27034  ftalem1  27039  ftalem5  27043  basellem3  27049  basellem5  27051  mpodvdsmulf1o  27160  dvdsmulf1o  27162  sgmppw  27164  logfac2  27184  chpval2  27185  chpchtsum  27186  perfect1  27195  lgsdirprm  27298  lgsdi  27301  lgsdirnn0  27311  lgsdinn0  27312  gausslemma2dlem1a  27332  gausslemma2dlem6  27339  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  lgsquad2  27353  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgslem3d1  27370  2lgsoddprmlem2  27376  2sqlem3  27387  2sqlem4  27388  2sqmod  27403  chebbnd1lem2  27437  chebbnd1lem3  27438  chtppilimlem2  27441  chto1lb  27445  rplogsumlem1  27451  dchrisumlem2  27457  dchrvmasum2lem  27463  dchrisum0flblem2  27476  dchrisum0lem2a  27484  mulogsumlem  27498  mulog2sumlem2  27502  selberglem1  27512  selberg2lem  27517  selberg3lem1  27524  selberg4  27528  pntrsumo1  27532  selberg34r  27538  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntlemb  27564  pntlemq  27568  pntlemr  27569  pntlemj  27570  pntlemo  27574  pnt2  27580  pnt  27581  padicabvcxp  27599  ostth2lem2  27601  ostth2lem3  27602  ostth2lem4  27603  ttgcontlem1  28957  brbtwn2  28978  colinearalglem1  28979  colinearalg  28983  axpaschlem  29013  axcontlem8  29044  numclwwlk1  30436  numclwwlk7  30466  smcnlem  30772  pjhthlem1  31466  kbmul  32030  kbass2  32192  submuladdd  32819  muldivdid  32820  pythagreim  32825  quad3d  32829  sgnmul  32916  2exple2exp  32926  psgnfzto1st  33187  zringfrac  33635  ccfldextdgrr  33829  fldext2rspun  33839  fldext2chn  33885  constrrtlc1  33889  constrrtcclem  33891  constrrtcc  33892  constrremulcl  33924  constrmulcl  33928  cos9thpiminplylem1  33939  qqhval2lem  34138  qqhghm  34145  qqhrhm  34146  oddpwdc  34511  plymulx0  34704  signsvtp  34740  signsvtn  34741  signsvfpn  34742  signsvfnn  34743  breprexplemc  34789  circlemethhgt  34800  logdivsqrle  34807  hgt750lemf  34810  hgt750lemb  34813  hgt750leme  34815  subfacval2  35381  subfaclim  35382  fwddifnp1  36359  knoppndvlem11  36722  knoppndvlem17  36728  bj-subcom  37513  bj-bary1lem1  37516  itg2addnclem  37872  itg2addnclem2  37873  itgabsnc  37890  ftc1cnnclem  37892  areacirclem1  37909  areacirc  37914  geomcau  37960  bfplem1  38023  rrndstprj2  38032  rrnequiv  38036  lcmineqlem1  42283  lcmineqlem5  42287  lcmineqlem8  42290  lcmineqlem11  42293  lcmineqlem18  42300  lcmineqlem21  42303  3lexlogpow5ineq2  42309  3lexlogpow2ineq1  42312  dvrelogpow2b  42322  aks4d1p1p7  42328  primrootscoprmpow  42353  primrootscoprbij  42356  aks6d1c1  42370  aks6d1c2  42384  2np3bcnp1  42398  2ap1caineq  42399  bcle2d  42433  aks6d1c7lem1  42434  nicomachus  42567  retire  42574  readvrec  42617  3cubeslem2  42927  3cubeslem3l  42928  3cubeslem3r  42929  irrapxlem5  43068  pellexlem2  43072  pellexlem6  43076  qirropth  43150  rmxyadd  43163  rmxm1  43176  rmxluc  43178  rmyluc2  43180  rmydbl  43182  jm2.24nn  43201  jm2.17a  43202  jm2.17b  43203  jm2.17c  43204  jm2.18  43230  jm2.19lem2  43232  jm2.22  43237  jm2.23  43238  areaquad  43458  imo72b2  44413  int-mulcomd  44417  int-rightdistd  44421  cvgdvgrat  44554  radcnvrat  44555  bccm1k  44583  binomcxplemwb  44589  binomcxplemnotnn0  44597  sineq0ALT  45177  mul13d  45528  divdiv3d  45604  mccllem  45843  coskpi2  46110  cosknegpi  46113  dvsinax  46157  dvasinbx  46164  dvcosax  46170  dvnxpaek  46186  dvnmul  46187  dvnprodlem2  46191  itgsinexplem1  46198  stoweidlem1  46245  stoweidlem11  46255  stoweidlem26  46270  stoweidlem32  46276  wallispilem4  46312  wallispi2lem1  46315  wallispi2lem2  46316  stirlinglem3  46320  stirlinglem4  46321  stirlinglem5  46322  stirlinglem7  46324  stirlinglem10  46327  stirlinglem15  46332  dirkertrigeqlem1  46342  dirkertrigeqlem2  46343  dirkertrigeqlem3  46344  dirkertrigeq  46345  dirkercncflem1  46347  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem56  46406  fourierdlem66  46416  fourierdlem83  46433  fourierswlem  46474  fouriersw  46475  etransclem23  46501  etransclem24  46502  etransclem38  46516  etransclem46  46524  hoiprodp1  46832  hoidmvlelem2  46840  smfmullem1  47035  sigarac  47096  sigarls  47101  sigarid  47102  sigardiv  47105  sigarcol  47108  sigaradd  47110  cevathlem1  47111  sqrtnegnre  47553  fmtnoodd  47779  sqrtpwpw2p  47784  fmtnorec3  47794  fmtnoprmfac2lem1  47812  fmtnofac1  47816  lighneallem2  47852  lighneallem3  47853  proththd  47860  requad01  47867  dfeven2  47895  fppr2odd  47977  fpprwppr  47985  altgsumbc  48598  altgsumbcALT  48599  blennnt2  48835  dignn0flhalflem2  48862  dignn0ehalf  48863  itcovalt2lem2lem2  48920  affinecomb2  48949  rrx2linest  48988  itscnhlc0yqe  49005  itsclc0yqsollem1  49008  itscnhlc0xyqsol  49011  itschlc0xyqsol1  49012  itsclc0xyqsolr  49015  itsclquadb  49022  2itscplem3  49026  itscnhlinecirc02plem1  49028  itscnhlinecirc02plem2  49029  inlinecirc02p  49033  amgmwlem  50047