Theorem mulcomd 11302

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7408  ℂcc 11170   · cmul 11177

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 11236

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mul31  11449  mul4r  11451  mulcand  11919  mulcan2d  11920  divcan1  11953  divrec2  11961  div23  11963  muldivdid  11981  divdivdiv  11988  divmuleq  11992  divadddiv  12002  divcan5rd  12090  dmdcan2d  12093  mvllmuld  12119  rdiv  12122  subhalfhalf  12550  mul2lt0llt0  13196  mul2lt0lgt0  13197  prodge0ld  13200  xmulcom  13366  modvalr  13981  mulp1mod1  14023  modmul12d  14037  modnegd  14038  modmulmodr  14049  expaddz  14218  binom3  14336  expmulnbnd  14347  digit1  14349  bccmpl  14421  bcm1k  14427  bcn2  14431  bcpasc  14433  sgnmul  15228  recval  15458  abs1m  15471  bhmafibid1cn  15601  bhmafibid2cn  15602  reccn2  15732  lo1mul2  15764  isummulc1  15897  fsummulc1  15919  incexclem  15973  incexc  15974  trireciplem  15999  pwdif  16005  geolim  16007  cvgrat  16020  mertens  16023  ntrivcvgmul  16039  fallfacfwd  16170  bpoly4  16193  fsumcube  16194  eftlub  16245  sinadd  16300  cosadd  16301  sin2t  16313  nndivides  16400  dvds2ln  16427  even2n  16480  oddm1even  16481  mod2eq1n2dvds  16485  m1exp1  16514  pwp1fsum  16529  divalgmod  16544  bitsp1  16569  bitsinv1lem  16579  sadadd2lem  16597  smumullem  16630  gcdmultiplez  16673  mulgcdr  16688  rplpwr  16696  lcmgcdlem  16744  divgcdcoprmex  16804  cncongr1  16805  eulerthlem2  16921  prmdiv  16924  prmdivdiv  16926  vfermltlALT  16942  modprmn0modprm0  16947  coprimeprodsq  16948  pythagtriplem6  16961  pythagtriplem7  16962  pceulem  16985  pcadd  17029  prmpwdvds  17044  mul4sqlem  17093  4sqlem17  17101  mulgassr  19284  odmodnn0  19716  odmulg  19732  odmulgeq  19733  odbezout  19734  odadd1  20024  ablfacrp2  20245  pgpfac1lem3  20255  zringlpirlem3  21732  znunit  21831  icopnfhmeo  25226  cphassr  25495  pjthlem1  25720  itgabs  26117  dvmulbr  26221  dvcmul  26226  dvcmulf  26227  dvmptcmul  26246  cmvth  26273  dvlipcn  26276  c1liplem1  26278  lhop1lem  26295  lhop2  26297  dvcvx  26302  dvfsumlem2  26309  ftc1lem4  26321  itgparts  26329  plyn0mulidp  26566  dvply1  26569  elqaalem3  26608  aalioulem4  26626  taylthlem2  26665  abelthlem6  26727  abelthlem7  26729  tangtx  26798  tanarg  26911  advlogexp  26947  mulcxp  26977  cxpmul  26980  abscxp  26984  dvcxp2  27033  cxpeq  27049  ang180lem1  27101  lawcoslem1  27107  lawcos  27108  heron  27130  dcubic1  27137  mcubic  27139  cubic2  27140  binom4  27142  dquart  27145  quart1lem  27147  quart1  27148  quartlem1  27149  dvatan  27227  leibpi  27234  log2cnv  27236  efrlim  27261  cxp2lim  27268  cxploglim  27269  zetacvg  27306  lgamgulmlem2  27321  lgamgulmlem3  27322  wilthlem1  27359  ftalem1  27364  ftalem5  27368  basellem3  27374  basellem5  27376  basellem8  27379  mpodvdsmulf1o  27485  dvdsmulf1o  27487  sgmppw  27488  logfac2  27508  chpval2  27509  chpchtsum  27510  perfect1  27519  lgsdirprm  27622  lgsdi  27625  lgsdirnn0  27635  lgsdinn0  27636  gausslemma2dlem1a  27656  gausslemma2dlem6  27663  lgsquadlem1  27671  lgsquadlem2  27672  lgsquadlem3  27673  lgsquad2  27677  2lgslem3a1  27691  2lgslem3b1  27692  2lgslem3c1  27693  2lgslem3d1  27694  2lgsoddprmlem2  27700  2sqlem3  27711  2sqlem4  27712  2sqmod  27727  chebbnd1lem2  27761  chebbnd1lem3  27762  chtppilimlem2  27765  chto1lb  27769  rplogsumlem1  27775  dchrisumlem2  27781  dchrvmasum2lem  27787  dchrisum0flblem2  27800  dchrisum0lem2a  27808  mulogsumlem  27822  mulog2sumlem2  27826  selberglem1  27836  selberg2lem  27841  selberg3lem1  27848  selberg4  27852  pntrsumo1  27856  selberg34r  27862  pntrlog2bndlem3  27870  pntrlog2bndlem4  27871  pntlemb  27888  pntlemq  27892  pntlemr  27893  pntlemj  27894  pntlemo  27898  pnt2  27904  pnt  27905  padicabvcxp  27923  ostth2lem2  27925  ostth2lem3  27926  ostth2lem4  27927  ttgcontlem1  29396  brbtwn2  29417  colinearalglem1  29418  colinearalg  29422  axpaschlem  29452  axcontlem8  29483  numclwwlk1  30896  numclwwlk7  30926  smcnlem  31233  pjhthlem1  31927  kbmul  32491  kbass2  32653  submuladdd  33266  pythagreim  33271  quad3d  33275  2exple2exp  33359  psgnfzto1st  33600  zringfrac  34020  ccfldextdgrr  34238  fldext2rspun  34248  fldext2chn  34294  constrrtlc1  34298  constrrtcclem  34300  constrrtcc  34301  constrremulcl  34333  constrmulcl  34337  cos9thpiminplylem1  34348  qqhval2lem  34547  qqhghm  34554  qqhrhm  34555  oddpwdc  34921  signsvtp  35147  signsvtn  35148  signsvfpn  35149  signsvfnn  35150  breprexplemc  35196  circlemethhgt  35207  logdivsqrle  35214  hgt750lemf  35217  hgt750lemb  35220  hgt750leme  35222  subfacval2  35873  subfaclim  35874  fwddifnp1  36852  knoppndvlem11  37310  knoppndvlem17  37316  bj-subcom  38149  bj-bary1lem1  38152  itg2addnclem  38509  itg2addnclem2  38510  itgabsnc  38527  ftc1cnnclem  38529  areacirclem1  38546  areacirc  38551  geomcau  38613  bfplem1  38676  rrndstprj2  38685  rrnequiv  38689  lcmineqlem1  42999  lcmineqlem5  43003  lcmineqlem8  43006  lcmineqlem11  43009  lcmineqlem18  43016  lcmineqlem21  43019  3lexlogpow5ineq2  43025  3lexlogpow2ineq1  43028  dvrelogpow2b  43038  aks4d1p1p7  43044  primrootscoprmpow  43069  primrootscoprbij  43072  aks6d1c1  43086  aks6d1c2  43100  2np3bcnp1  43114  2ap1caineq  43115  bcle2d  43149  aks6d1c7lem1  43150  quadfac  43175  nicomachus  43291  retire  43298  readvrec  43341  3cubeslem2  43634  3cubeslem3l  43635  3cubeslem3r  43636  irrapxlem5  43771  pellexlem2  43775  pellexlem6  43779  qirropth  43853  rmxyadd  43866  rmxm1  43879  rmxluc  43881  rmyluc2  43883  rmydbl  43885  jm2.24nn  43904  jm2.17a  43905  jm2.17b  43906  jm2.17c  43907  jm2.18  43933  jm2.19lem2  43935  jm2.22  43940  jm2.23  43941  areaquad  44161  imo72b2  45116  int-mulcomd  45120  int-rightdistd  45124  cvgdvgrat  45241  radcnvrat  45242  bccm1k  45270  binomcxplemwb  45276  binomcxplemnotnn0  45284  sineq0ALT  45863  mul13d  46217  divdiv3d  46293  mccllem  46531  coskpi2  46798  cosknegpi  46801  dvsinax  46845  dvasinbx  46852  dvcosax  46858  dvnxpaek  46874  dvnmul  46875  dvnprodlem2  46879  itgsinexplem1  46886  stoweidlem1  46933  stoweidlem11  46943  stoweidlem26  46958  stoweidlem32  46964  wallispilem4  47000  wallispi2lem1  47003  wallispi2lem2  47004  stirlinglem3  47008  stirlinglem4  47009  stirlinglem5  47010  stirlinglem7  47012  stirlinglem10  47015  stirlinglem15  47020  dirkertrigeqlem1  47030  dirkertrigeqlem2  47031  dirkertrigeqlem3  47032  dirkertrigeq  47033  dirkercncflem1  47035  fourierdlem16  47055  fourierdlem21  47060  fourierdlem22  47061  fourierdlem56  47094  fourierdlem66  47104  fourierdlem83  47121  fourierswlem  47162  fouriersw  47163  etransclem23  47189  etransclem24  47190  etransclem38  47204  etransclem46  47212  hoiprodp1  47520  hoidmvlelem2  47528  smfmullem1  47723  sigarac  47784  sigarls  47789  sigarid  47790  sigardiv  47793  sigarcol  47796  sigaradd  47798  cevathlem1  47799  sin3t  47839  cos3t  47840  sin5tlem1  47841  sin5tlem3  47843  sqrtnegnre  48299  fmtnoodd  48540  sqrtpwpw2p  48545  fmtnorec3  48555  fmtnoprmfac2lem1  48573  fmtnofac1  48577  lighneallem2  48613  lighneallem3  48614  proththd  48621  requad01  48641  dfeven2  48669  fppr2odd  48751  fpprwppr  48759  altgsumbc  49386  altgsumbcALT  49387  blennnt2  49623  dignn0flhalflem2  49650  dignn0ehalf  49651  itcovalt2lem2lem2  49708  affinecomb2  49737  rrx2linest  49776  itscnhlc0yqe  49793  itsclc0yqsollem1  49796  itscnhlc0xyqsol  49799  itschlc0xyqsol1  49800  itsclc0xyqsolr  49803  itsclquadb  49810  2itscplem3  49814  itscnhlinecirc02plem1  49816  itscnhlinecirc02plem2  49817  inlinecirc02p  49821  crosspaltd  50888  crossp3d  50889  amgmwlem  50909