Theorem mulcomd 11282

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   · cmul 11160

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

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

This theorem is referenced by:  mul31  11428  mul4r  11430  mulcand  11896  mulcan2d  11897  divcan1  11931  divrec2  11939  div23  11941  divdivdiv  11968  divmuleq  11972  divadddiv  11982  divcan5rd  12070  dmdcan2d  12073  mvllmuld  12099  rdiv  12102  subhalfhalf  12500  mul2lt0llt0  13139  mul2lt0lgt0  13140  prodge0ld  13143  xmulcom  13308  modvalr  13912  mulp1mod1  13952  modmul12d  13966  modnegd  13967  modmulmodr  13978  expaddz  14147  binom3  14263  expmulnbnd  14274  digit1  14276  bccmpl  14348  bcm1k  14354  bcn2  14358  bcpasc  14360  recval  15361  abs1m  15374  bhmafibid1cn  15502  bhmafibid2cn  15503  reccn2  15633  lo1mul2  15665  isummulc1  15799  fsummulc1  15821  incexclem  15872  incexc  15873  trireciplem  15898  pwdif  15904  geolim  15906  cvgrat  15919  mertens  15922  ntrivcvgmul  15938  fallfacfwd  16072  bpoly4  16095  fsumcube  16096  eftlub  16145  sinadd  16200  cosadd  16201  sin2t  16213  nndivides  16300  dvds2ln  16326  even2n  16379  oddm1even  16380  mod2eq1n2dvds  16384  m1exp1  16413  pwp1fsum  16428  divalgmod  16443  bitsp1  16468  bitsinv1lem  16478  sadadd2lem  16496  smumullem  16529  gcdmultiplez  16572  mulgcdr  16587  rplpwr  16595  lcmgcdlem  16643  divgcdcoprmex  16703  cncongr1  16704  eulerthlem2  16819  prmdiv  16822  prmdivdiv  16824  vfermltlALT  16840  modprmn0modprm0  16845  coprimeprodsq  16846  pythagtriplem6  16859  pythagtriplem7  16860  pceulem  16883  pcadd  16927  prmpwdvds  16942  mul4sqlem  16991  4sqlem17  16999  mulgassr  19130  odmodnn0  19558  odmulg  19574  odmulgeq  19575  odbezout  19576  odadd1  19866  ablfacrp2  20087  pgpfac1lem3  20097  zringlpirlem3  21475  znunit  21582  icopnfhmeo  24974  cphassr  25246  pjthlem1  25471  itgabs  25870  dvmulbr  25975  dvmulbrOLD  25976  dvcmul  25981  dvcmulf  25982  dvmptcmul  26002  cmvth  26029  cmvthOLD  26030  dvlipcn  26033  c1liplem1  26035  lhop1lem  26052  lhop2  26054  dvcvx  26059  dvfsumlem2  26067  dvfsumlem2OLD  26068  ftc1lem4  26080  itgparts  26088  dvply1  26325  elqaalem3  26363  aalioulem4  26377  taylthlem2  26416  taylthlem2OLD  26417  abelthlem6  26480  abelthlem7  26482  tangtx  26547  tanarg  26661  advlogexp  26697  mulcxp  26727  cxpmul  26730  abscxp  26734  dvcxp2  26783  cxpeq  26800  ang180lem1  26852  lawcoslem1  26858  lawcos  26859  heron  26881  dcubic1  26888  mcubic  26890  cubic2  26891  binom4  26893  dquart  26896  quart1lem  26898  quart1  26899  quartlem1  26900  dvatan  26978  leibpi  26985  log2cnv  26987  efrlim  27012  efrlimOLD  27013  cxp2lim  27020  cxploglim  27021  zetacvg  27058  lgamgulmlem2  27073  lgamgulmlem3  27074  wilthlem1  27111  ftalem1  27116  ftalem5  27120  basellem3  27126  basellem5  27128  mpodvdsmulf1o  27237  dvdsmulf1o  27239  sgmppw  27241  logfac2  27261  chpval2  27262  chpchtsum  27263  perfect1  27272  lgsdirprm  27375  lgsdi  27378  lgsdirnn0  27388  lgsdinn0  27389  gausslemma2dlem1a  27409  gausslemma2dlem6  27416  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  lgsquad2  27430  2lgslem3a1  27444  2lgslem3b1  27445  2lgslem3c1  27446  2lgslem3d1  27447  2lgsoddprmlem2  27453  2sqlem3  27464  2sqlem4  27465  2sqmod  27480  chebbnd1lem2  27514  chebbnd1lem3  27515  chtppilimlem2  27518  chto1lb  27522  rplogsumlem1  27528  dchrisumlem2  27534  dchrvmasum2lem  27540  dchrisum0flblem2  27553  dchrisum0lem2a  27561  mulogsumlem  27575  mulog2sumlem2  27579  selberglem1  27589  selberg2lem  27594  selberg3lem1  27601  selberg4  27605  pntrsumo1  27609  selberg34r  27615  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntlemb  27641  pntlemq  27645  pntlemr  27646  pntlemj  27647  pntlemo  27651  pnt2  27657  pnt  27658  padicabvcxp  27676  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ttgcontlem1  28899  brbtwn2  28920  colinearalglem1  28921  colinearalg  28925  axpaschlem  28955  axcontlem8  28986  numclwwlk1  30380  numclwwlk7  30410  smcnlem  30716  pjhthlem1  31410  kbmul  31974  kbass2  32136  submuladdd  32750  muldivdid  32751  quad3d  32754  2exple2exp  32834  psgnfzto1st  33125  zringfrac  33582  ccfldextdgrr  33722  fldext2rspun  33732  fldext2chn  33769  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  qqhval2lem  33982  qqhghm  33989  qqhrhm  33990  oddpwdc  34356  sgnmul  34545  plymulx0  34562  signsvtp  34598  signsvtn  34599  signsvfpn  34600  signsvfnn  34601  breprexplemc  34647  circlemethhgt  34658  logdivsqrle  34665  hgt750lemf  34668  hgt750lemb  34671  hgt750leme  34673  subfacval2  35192  subfaclim  35193  fwddifnp1  36166  knoppndvlem11  36523  knoppndvlem17  36529  bj-subcom  37309  bj-bary1lem1  37312  itg2addnclem  37678  itg2addnclem2  37679  itgabsnc  37696  ftc1cnnclem  37698  areacirclem1  37715  areacirc  37720  geomcau  37766  bfplem1  37829  rrndstprj2  37838  rrnequiv  37842  lcmineqlem1  42030  lcmineqlem5  42034  lcmineqlem8  42037  lcmineqlem11  42040  lcmineqlem18  42047  lcmineqlem21  42050  3lexlogpow5ineq2  42056  3lexlogpow2ineq1  42059  dvrelogpow2b  42069  aks4d1p1p7  42075  primrootscoprmpow  42100  primrootscoprbij  42103  aks6d1c1  42117  aks6d1c2  42131  2np3bcnp1  42145  2ap1caineq  42146  bcle2d  42180  aks6d1c7lem1  42181  nicomachus  42346  retire  42354  readvrec  42392  3cubeslem2  42696  3cubeslem3l  42697  3cubeslem3r  42698  irrapxlem5  42837  pellexlem2  42841  pellexlem6  42845  qirropth  42919  rmxyadd  42933  rmxm1  42946  rmxluc  42948  rmyluc2  42950  rmydbl  42952  jm2.24nn  42971  jm2.17a  42972  jm2.17b  42973  jm2.17c  42974  jm2.18  43000  jm2.19lem2  43002  jm2.22  43007  jm2.23  43008  areaquad  43228  imo72b2  44185  int-mulcomd  44189  int-rightdistd  44193  cvgdvgrat  44332  radcnvrat  44333  bccm1k  44361  binomcxplemwb  44367  binomcxplemnotnn0  44375  sineq0ALT  44957  mul13d  45291  divdiv3d  45370  mccllem  45612  coskpi2  45881  cosknegpi  45884  dvsinax  45928  dvasinbx  45935  dvcosax  45941  dvnxpaek  45957  dvnmul  45958  dvnprodlem2  45962  itgsinexplem1  45969  stoweidlem1  46016  stoweidlem11  46026  stoweidlem26  46041  stoweidlem32  46047  wallispilem4  46083  wallispi2lem1  46086  wallispi2lem2  46087  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem7  46095  stirlinglem10  46098  stirlinglem15  46103  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem1  46118  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem56  46177  fourierdlem66  46187  fourierdlem83  46204  fourierswlem  46245  fouriersw  46246  etransclem23  46272  etransclem24  46273  etransclem38  46287  etransclem46  46295  hoiprodp1  46603  hoidmvlelem2  46611  smfmullem1  46806  sigarac  46867  sigarls  46872  sigarid  46873  sigardiv  46876  sigarcol  46879  sigaradd  46881  cevathlem1  46882  sqrtnegnre  47319  fmtnoodd  47520  sqrtpwpw2p  47525  fmtnorec3  47535  fmtnoprmfac2lem1  47553  fmtnofac1  47557  lighneallem2  47593  lighneallem3  47594  proththd  47601  requad01  47608  dfeven2  47636  fppr2odd  47718  fpprwppr  47726  altgsumbc  48268  altgsumbcALT  48269  blennnt2  48510  dignn0flhalflem2  48537  dignn0ehalf  48538  itcovalt2lem2lem2  48595  affinecomb2  48624  rrx2linest  48663  itscnhlc0yqe  48680  itsclc0yqsollem1  48683  itscnhlc0xyqsol  48686  itschlc0xyqsol1  48687  itsclc0xyqsolr  48690  itsclquadb  48697  2itscplem3  48701  itscnhlinecirc02plem1  48703  itscnhlinecirc02plem2  48704  inlinecirc02p  48708  amgmwlem  49321