Theorem mulcomd 11195

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

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

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

This theorem is referenced by:  mul31  11341  mul4r  11343  mulcand  11811  mulcan2d  11812  divcan1  11846  divrec2  11854  div23  11856  divdivdiv  11883  divmuleq  11887  divadddiv  11897  divcan5rd  11985  dmdcan2d  11988  mvllmuld  12014  rdiv  12017  subhalfhalf  12416  mul2lt0llt0  13057  mul2lt0lgt0  13058  prodge0ld  13061  xmulcom  13226  modvalr  13834  mulp1mod1  13876  modmul12d  13890  modnegd  13891  modmulmodr  13902  expaddz  14071  binom3  14189  expmulnbnd  14200  digit1  14202  bccmpl  14274  bcm1k  14280  bcn2  14284  bcpasc  14286  recval  15289  abs1m  15302  bhmafibid1cn  15432  bhmafibid2cn  15433  reccn2  15563  lo1mul2  15595  isummulc1  15729  fsummulc1  15751  incexclem  15802  incexc  15803  trireciplem  15828  pwdif  15834  geolim  15836  cvgrat  15849  mertens  15852  ntrivcvgmul  15868  fallfacfwd  16002  bpoly4  16025  fsumcube  16026  eftlub  16077  sinadd  16132  cosadd  16133  sin2t  16145  nndivides  16232  dvds2ln  16259  even2n  16312  oddm1even  16313  mod2eq1n2dvds  16317  m1exp1  16346  pwp1fsum  16361  divalgmod  16376  bitsp1  16401  bitsinv1lem  16411  sadadd2lem  16429  smumullem  16462  gcdmultiplez  16505  mulgcdr  16520  rplpwr  16528  lcmgcdlem  16576  divgcdcoprmex  16636  cncongr1  16637  eulerthlem2  16752  prmdiv  16755  prmdivdiv  16757  vfermltlALT  16773  modprmn0modprm0  16778  coprimeprodsq  16779  pythagtriplem6  16792  pythagtriplem7  16793  pceulem  16816  pcadd  16860  prmpwdvds  16875  mul4sqlem  16924  4sqlem17  16932  mulgassr  19044  odmodnn0  19470  odmulg  19486  odmulgeq  19487  odbezout  19488  odadd1  19778  ablfacrp2  19999  pgpfac1lem3  20009  zringlpirlem3  21374  znunit  21473  icopnfhmeo  24841  cphassr  25112  pjthlem1  25337  itgabs  25736  dvmulbr  25841  dvmulbrOLD  25842  dvcmul  25847  dvcmulf  25848  dvmptcmul  25868  cmvth  25895  cmvthOLD  25896  dvlipcn  25899  c1liplem1  25901  lhop1lem  25918  lhop2  25920  dvcvx  25925  dvfsumlem2  25933  dvfsumlem2OLD  25934  ftc1lem4  25946  itgparts  25954  dvply1  26191  elqaalem3  26229  aalioulem4  26243  taylthlem2  26282  taylthlem2OLD  26283  abelthlem6  26346  abelthlem7  26348  tangtx  26414  tanarg  26528  advlogexp  26564  mulcxp  26594  cxpmul  26597  abscxp  26601  dvcxp2  26650  cxpeq  26667  ang180lem1  26719  lawcoslem1  26725  lawcos  26726  heron  26748  dcubic1  26755  mcubic  26757  cubic2  26758  binom4  26760  dquart  26763  quart1lem  26765  quart1  26766  quartlem1  26767  dvatan  26845  leibpi  26852  log2cnv  26854  efrlim  26879  efrlimOLD  26880  cxp2lim  26887  cxploglim  26888  zetacvg  26925  lgamgulmlem2  26940  lgamgulmlem3  26941  wilthlem1  26978  ftalem1  26983  ftalem5  26987  basellem3  26993  basellem5  26995  mpodvdsmulf1o  27104  dvdsmulf1o  27106  sgmppw  27108  logfac2  27128  chpval2  27129  chpchtsum  27130  perfect1  27139  lgsdirprm  27242  lgsdi  27245  lgsdirnn0  27255  lgsdinn0  27256  gausslemma2dlem1a  27276  gausslemma2dlem6  27283  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  lgsquad2  27297  2lgslem3a1  27311  2lgslem3b1  27312  2lgslem3c1  27313  2lgslem3d1  27314  2lgsoddprmlem2  27320  2sqlem3  27331  2sqlem4  27332  2sqmod  27347  chebbnd1lem2  27381  chebbnd1lem3  27382  chtppilimlem2  27385  chto1lb  27389  rplogsumlem1  27395  dchrisumlem2  27401  dchrvmasum2lem  27407  dchrisum0flblem2  27420  dchrisum0lem2a  27428  mulogsumlem  27442  mulog2sumlem2  27446  selberglem1  27456  selberg2lem  27461  selberg3lem1  27468  selberg4  27472  pntrsumo1  27476  selberg34r  27482  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntlemb  27508  pntlemq  27512  pntlemr  27513  pntlemj  27514  pntlemo  27518  pnt2  27524  pnt  27525  padicabvcxp  27543  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  ttgcontlem1  28812  brbtwn2  28832  colinearalglem1  28833  colinearalg  28837  axpaschlem  28867  axcontlem8  28898  numclwwlk1  30290  numclwwlk7  30320  smcnlem  30626  pjhthlem1  31320  kbmul  31884  kbass2  32046  submuladdd  32663  muldivdid  32664  pythagreim  32669  quad3d  32673  sgnmul  32760  2exple2exp  32770  psgnfzto1st  33062  zringfrac  33525  ccfldextdgrr  33667  fldext2rspun  33677  fldext2chn  33718  constrrtlc1  33722  constrrtcclem  33724  constrrtcc  33725  constrremulcl  33757  constrmulcl  33761  cos9thpiminplylem1  33772  qqhval2lem  33971  qqhghm  33978  qqhrhm  33979  oddpwdc  34345  plymulx0  34538  signsvtp  34574  signsvtn  34575  signsvfpn  34576  signsvfnn  34577  breprexplemc  34623  circlemethhgt  34634  logdivsqrle  34641  hgt750lemf  34644  hgt750lemb  34647  hgt750leme  34649  subfacval2  35174  subfaclim  35175  fwddifnp1  36153  knoppndvlem11  36510  knoppndvlem17  36516  bj-subcom  37296  bj-bary1lem1  37299  itg2addnclem  37665  itg2addnclem2  37666  itgabsnc  37683  ftc1cnnclem  37685  areacirclem1  37702  areacirc  37707  geomcau  37753  bfplem1  37816  rrndstprj2  37825  rrnequiv  37829  lcmineqlem1  42017  lcmineqlem5  42021  lcmineqlem8  42024  lcmineqlem11  42027  lcmineqlem18  42034  lcmineqlem21  42037  3lexlogpow5ineq2  42043  3lexlogpow2ineq1  42046  dvrelogpow2b  42056  aks4d1p1p7  42062  primrootscoprmpow  42087  primrootscoprbij  42090  aks6d1c1  42104  aks6d1c2  42118  2np3bcnp1  42132  2ap1caineq  42133  bcle2d  42167  aks6d1c7lem1  42168  nicomachus  42300  retire  42307  readvrec  42350  3cubeslem2  42673  3cubeslem3l  42674  3cubeslem3r  42675  irrapxlem5  42814  pellexlem2  42818  pellexlem6  42822  qirropth  42896  rmxyadd  42910  rmxm1  42923  rmxluc  42925  rmyluc2  42927  rmydbl  42929  jm2.24nn  42948  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  jm2.18  42977  jm2.19lem2  42979  jm2.22  42984  jm2.23  42985  areaquad  43205  imo72b2  44161  int-mulcomd  44165  int-rightdistd  44169  cvgdvgrat  44302  radcnvrat  44303  bccm1k  44331  binomcxplemwb  44337  binomcxplemnotnn0  44345  sineq0ALT  44926  mul13d  45278  divdiv3d  45355  mccllem  45595  coskpi2  45864  cosknegpi  45867  dvsinax  45911  dvasinbx  45918  dvcosax  45924  dvnxpaek  45940  dvnmul  45941  dvnprodlem2  45945  itgsinexplem1  45952  stoweidlem1  45999  stoweidlem11  46009  stoweidlem26  46024  stoweidlem32  46030  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem7  46078  stirlinglem10  46081  stirlinglem15  46086  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem1  46101  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem56  46160  fourierdlem66  46170  fourierdlem83  46187  fourierswlem  46228  fouriersw  46229  etransclem23  46255  etransclem24  46256  etransclem38  46270  etransclem46  46278  hoiprodp1  46586  hoidmvlelem2  46594  smfmullem1  46789  sigarac  46850  sigarls  46855  sigarid  46856  sigardiv  46859  sigarcol  46862  sigaradd  46864  cevathlem1  46865  sqrtnegnre  47308  fmtnoodd  47534  sqrtpwpw2p  47539  fmtnorec3  47549  fmtnoprmfac2lem1  47567  fmtnofac1  47571  lighneallem2  47607  lighneallem3  47608  proththd  47615  requad01  47622  dfeven2  47650  fppr2odd  47732  fpprwppr  47740  altgsumbc  48340  altgsumbcALT  48341  blennnt2  48578  dignn0flhalflem2  48605  dignn0ehalf  48606  itcovalt2lem2lem2  48663  affinecomb2  48692  rrx2linest  48731  itscnhlc0yqe  48748  itsclc0yqsollem1  48751  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itsclc0xyqsolr  48758  itsclquadb  48765  2itscplem3  48769  itscnhlinecirc02plem1  48771  itscnhlinecirc02plem2  48772  inlinecirc02p  48776  amgmwlem  49791