Theorem mulcomd 11254

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   · cmul 11132

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

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

This theorem is referenced by:  mul31  11400  mul4r  11402  mulcand  11868  mulcan2d  11869  divcan1  11903  divrec2  11911  div23  11913  divdivdiv  11940  divmuleq  11944  divadddiv  11954  divcan5rd  12042  dmdcan2d  12045  mvllmuld  12071  rdiv  12074  subhalfhalf  12473  mul2lt0llt0  13111  mul2lt0lgt0  13112  prodge0ld  13115  xmulcom  13280  modvalr  13887  mulp1mod1  13927  modmul12d  13941  modnegd  13942  modmulmodr  13953  expaddz  14122  binom3  14240  expmulnbnd  14251  digit1  14253  bccmpl  14325  bcm1k  14331  bcn2  14335  bcpasc  14337  recval  15339  abs1m  15352  bhmafibid1cn  15480  bhmafibid2cn  15481  reccn2  15611  lo1mul2  15643  isummulc1  15777  fsummulc1  15799  incexclem  15850  incexc  15851  trireciplem  15876  pwdif  15882  geolim  15884  cvgrat  15897  mertens  15900  ntrivcvgmul  15916  fallfacfwd  16050  bpoly4  16073  fsumcube  16074  eftlub  16125  sinadd  16180  cosadd  16181  sin2t  16193  nndivides  16280  dvds2ln  16306  even2n  16359  oddm1even  16360  mod2eq1n2dvds  16364  m1exp1  16393  pwp1fsum  16408  divalgmod  16423  bitsp1  16448  bitsinv1lem  16458  sadadd2lem  16476  smumullem  16509  gcdmultiplez  16552  mulgcdr  16567  rplpwr  16575  lcmgcdlem  16623  divgcdcoprmex  16683  cncongr1  16684  eulerthlem2  16799  prmdiv  16802  prmdivdiv  16804  vfermltlALT  16820  modprmn0modprm0  16825  coprimeprodsq  16826  pythagtriplem6  16839  pythagtriplem7  16840  pceulem  16863  pcadd  16907  prmpwdvds  16922  mul4sqlem  16971  4sqlem17  16979  mulgassr  19093  odmodnn0  19519  odmulg  19535  odmulgeq  19536  odbezout  19537  odadd1  19827  ablfacrp2  20048  pgpfac1lem3  20058  zringlpirlem3  21423  znunit  21522  icopnfhmeo  24890  cphassr  25162  pjthlem1  25387  itgabs  25786  dvmulbr  25891  dvmulbrOLD  25892  dvcmul  25897  dvcmulf  25898  dvmptcmul  25918  cmvth  25945  cmvthOLD  25946  dvlipcn  25949  c1liplem1  25951  lhop1lem  25968  lhop2  25970  dvcvx  25975  dvfsumlem2  25983  dvfsumlem2OLD  25984  ftc1lem4  25996  itgparts  26004  dvply1  26241  elqaalem3  26279  aalioulem4  26293  taylthlem2  26332  taylthlem2OLD  26333  abelthlem6  26396  abelthlem7  26398  tangtx  26464  tanarg  26578  advlogexp  26614  mulcxp  26644  cxpmul  26647  abscxp  26651  dvcxp2  26700  cxpeq  26717  ang180lem1  26769  lawcoslem1  26775  lawcos  26776  heron  26798  dcubic1  26805  mcubic  26807  cubic2  26808  binom4  26810  dquart  26813  quart1lem  26815  quart1  26816  quartlem1  26817  dvatan  26895  leibpi  26902  log2cnv  26904  efrlim  26929  efrlimOLD  26930  cxp2lim  26937  cxploglim  26938  zetacvg  26975  lgamgulmlem2  26990  lgamgulmlem3  26991  wilthlem1  27028  ftalem1  27033  ftalem5  27037  basellem3  27043  basellem5  27045  mpodvdsmulf1o  27154  dvdsmulf1o  27156  sgmppw  27158  logfac2  27178  chpval2  27179  chpchtsum  27180  perfect1  27189  lgsdirprm  27292  lgsdi  27295  lgsdirnn0  27305  lgsdinn0  27306  gausslemma2dlem1a  27326  gausslemma2dlem6  27333  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  lgsquad2  27347  2lgslem3a1  27361  2lgslem3b1  27362  2lgslem3c1  27363  2lgslem3d1  27364  2lgsoddprmlem2  27370  2sqlem3  27381  2sqlem4  27382  2sqmod  27397  chebbnd1lem2  27431  chebbnd1lem3  27432  chtppilimlem2  27435  chto1lb  27439  rplogsumlem1  27445  dchrisumlem2  27451  dchrvmasum2lem  27457  dchrisum0flblem2  27470  dchrisum0lem2a  27478  mulogsumlem  27492  mulog2sumlem2  27496  selberglem1  27506  selberg2lem  27511  selberg3lem1  27518  selberg4  27522  pntrsumo1  27526  selberg34r  27532  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntlemb  27558  pntlemq  27562  pntlemr  27563  pntlemj  27564  pntlemo  27568  pnt2  27574  pnt  27575  padicabvcxp  27593  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  ttgcontlem1  28810  brbtwn2  28830  colinearalglem1  28831  colinearalg  28835  axpaschlem  28865  axcontlem8  28896  numclwwlk1  30288  numclwwlk7  30318  smcnlem  30624  pjhthlem1  31318  kbmul  31882  kbass2  32044  submuladdd  32663  muldivdid  32664  pythagreim  32669  quad3d  32673  sgnmul  32760  2exple2exp  32770  psgnfzto1st  33062  zringfrac  33515  ccfldextdgrr  33659  fldext2rspun  33669  fldext2chn  33708  constrrtlc1  33712  constrrtcclem  33714  constrrtcc  33715  constrremulcl  33747  constrmulcl  33751  cos9thpiminplylem1  33762  qqhval2lem  33958  qqhghm  33965  qqhrhm  33966  oddpwdc  34332  plymulx0  34525  signsvtp  34561  signsvtn  34562  signsvfpn  34563  signsvfnn  34564  breprexplemc  34610  circlemethhgt  34621  logdivsqrle  34628  hgt750lemf  34631  hgt750lemb  34634  hgt750leme  34636  subfacval2  35155  subfaclim  35156  fwddifnp1  36129  knoppndvlem11  36486  knoppndvlem17  36492  bj-subcom  37272  bj-bary1lem1  37275  itg2addnclem  37641  itg2addnclem2  37642  itgabsnc  37659  ftc1cnnclem  37661  areacirclem1  37678  areacirc  37683  geomcau  37729  bfplem1  37792  rrndstprj2  37801  rrnequiv  37805  lcmineqlem1  41988  lcmineqlem5  41992  lcmineqlem8  41995  lcmineqlem11  41998  lcmineqlem18  42005  lcmineqlem21  42008  3lexlogpow5ineq2  42014  3lexlogpow2ineq1  42017  dvrelogpow2b  42027  aks4d1p1p7  42033  primrootscoprmpow  42058  primrootscoprbij  42061  aks6d1c1  42075  aks6d1c2  42089  2np3bcnp1  42103  2ap1caineq  42104  bcle2d  42138  aks6d1c7lem1  42139  nicomachus  42308  retire  42315  readvrec  42352  3cubeslem2  42655  3cubeslem3l  42656  3cubeslem3r  42657  irrapxlem5  42796  pellexlem2  42800  pellexlem6  42804  qirropth  42878  rmxyadd  42892  rmxm1  42905  rmxluc  42907  rmyluc2  42909  rmydbl  42911  jm2.24nn  42930  jm2.17a  42931  jm2.17b  42932  jm2.17c  42933  jm2.18  42959  jm2.19lem2  42961  jm2.22  42966  jm2.23  42967  areaquad  43187  imo72b2  44143  int-mulcomd  44147  int-rightdistd  44151  cvgdvgrat  44285  radcnvrat  44286  bccm1k  44314  binomcxplemwb  44320  binomcxplemnotnn0  44328  sineq0ALT  44909  mul13d  45256  divdiv3d  45334  mccllem  45574  coskpi2  45843  cosknegpi  45846  dvsinax  45890  dvasinbx  45897  dvcosax  45903  dvnxpaek  45919  dvnmul  45920  dvnprodlem2  45924  itgsinexplem1  45931  stoweidlem1  45978  stoweidlem11  45988  stoweidlem26  46003  stoweidlem32  46009  wallispilem4  46045  wallispi2lem1  46048  wallispi2lem2  46049  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem7  46057  stirlinglem10  46060  stirlinglem15  46065  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem1  46080  fourierdlem16  46100  fourierdlem21  46105  fourierdlem22  46106  fourierdlem56  46139  fourierdlem66  46149  fourierdlem83  46166  fourierswlem  46207  fouriersw  46208  etransclem23  46234  etransclem24  46235  etransclem38  46249  etransclem46  46257  hoiprodp1  46565  hoidmvlelem2  46573  smfmullem1  46768  sigarac  46829  sigarls  46834  sigarid  46835  sigardiv  46838  sigarcol  46841  sigaradd  46843  cevathlem1  46844  sqrtnegnre  47284  fmtnoodd  47495  sqrtpwpw2p  47500  fmtnorec3  47510  fmtnoprmfac2lem1  47528  fmtnofac1  47532  lighneallem2  47568  lighneallem3  47569  proththd  47576  requad01  47583  dfeven2  47611  fppr2odd  47693  fpprwppr  47701  altgsumbc  48275  altgsumbcALT  48276  blennnt2  48517  dignn0flhalflem2  48544  dignn0ehalf  48545  itcovalt2lem2lem2  48602  affinecomb2  48631  rrx2linest  48670  itscnhlc0yqe  48687  itsclc0yqsollem1  48690  itscnhlc0xyqsol  48693  itschlc0xyqsol1  48694  itsclc0xyqsolr  48697  itsclquadb  48704  2itscplem3  48708  itscnhlinecirc02plem1  48710  itscnhlinecirc02plem2  48711  inlinecirc02p  48715  amgmwlem  49614