Theorem mulcomd 11257

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 596	1 ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))

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

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

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

This theorem is used by:  mul31  11404  mul4r  11406  mulcand  11874  mulcan2d  11875  divcan1  11908  divrec2  11916  div23  11918  muldivdid  11936  divdivdiv  11943  divmuleq  11947  divadddiv  11957  divcan5rd  12045  dmdcan2d  12048  mvllmuld  12074  rdiv  12077  subhalfhalf  12505  mul2lt0llt0  13150  mul2lt0lgt0  13151  prodge0ld  13154  xmulcom  13320  modvalr  13935  mulp1mod1  13977  modmul12d  13991  modnegd  13992  modmulmodr  14003  expaddz  14172  binom3  14290  expmulnbnd  14301  digit1  14303  bccmpl  14375  bcm1k  14381  bcn2  14385  bcpasc  14387  sgnmul  15182  recval  15412  abs1m  15425  bhmafibid1cn  15555  bhmafibid2cn  15556  reccn2  15686  lo1mul2  15718  isummulc1  15851  fsummulc1  15873  incexclem  15927  incexc  15928  trireciplem  15953  pwdif  15959  geolim  15961  cvgrat  15974  mertens  15977  ntrivcvgmul  15993  fallfacfwd  16126  bpoly4  16149  fsumcube  16150  eftlub  16201  sinadd  16256  cosadd  16257  sin2t  16269  nndivides  16356  dvds2ln  16383  even2n  16436  oddm1even  16437  mod2eq1n2dvds  16441  m1exp1  16470  pwp1fsum  16485  divalgmod  16500  bitsp1  16525  bitsinv1lem  16535  sadadd2lem  16553  smumullem  16586  gcdmultiplez  16629  mulgcdr  16644  rplpwr  16652  lcmgcdlem  16700  divgcdcoprmex  16760  cncongr1  16761  eulerthlem2  16877  prmdiv  16880  prmdivdiv  16882  vfermltlALT  16898  modprmn0modprm0  16903  coprimeprodsq  16904  pythagtriplem6  16917  pythagtriplem7  16918  pceulem  16941  pcadd  16985  prmpwdvds  17000  mul4sqlem  17049  4sqlem17  17057  mulgassr  19239  odmodnn0  19671  odmulg  19687  odmulgeq  19688  odbezout  19689  odadd1  19979  ablfacrp2  20200  pgpfac1lem3  20210  zringlpirlem3  21681  znunit  21780  icopnfhmeo  25175  cphassr  25444  pjthlem1  25669  itgabs  26067  dvmulbr  26171  dvcmul  26176  dvcmulf  26177  dvmptcmul  26196  cmvth  26223  dvlipcn  26226  c1liplem1  26228  lhop1lem  26245  lhop2  26247  dvcvx  26252  dvfsumlem2  26259  ftc1lem4  26271  itgparts  26279  plyn0mulidp  26515  dvply1  26518  elqaalem3  26555  aalioulem4  26571  taylthlem2  26610  abelthlem6  26672  abelthlem7  26674  tangtx  26743  tanarg  26857  advlogexp  26893  mulcxp  26923  cxpmul  26926  abscxp  26930  dvcxp2  26979  cxpeq  26995  ang180lem1  27047  lawcoslem1  27053  lawcos  27054  heron  27076  dcubic1  27083  mcubic  27085  cubic2  27086  binom4  27088  dquart  27091  quart1lem  27093  quart1  27094  quartlem1  27095  dvatan  27173  leibpi  27180  log2cnv  27182  efrlim  27207  cxp2lim  27214  cxploglim  27215  zetacvg  27252  lgamgulmlem2  27267  lgamgulmlem3  27268  wilthlem1  27305  ftalem1  27310  ftalem5  27314  basellem3  27320  basellem5  27322  basellem8  27325  mpodvdsmulf1o  27431  dvdsmulf1o  27433  sgmppw  27434  logfac2  27454  chpval2  27455  chpchtsum  27456  perfect1  27465  lgsdirprm  27568  lgsdi  27571  lgsdirnn0  27581  lgsdinn0  27582  gausslemma2dlem1a  27602  gausslemma2dlem6  27609  lgsquadlem1  27617  lgsquadlem2  27618  lgsquadlem3  27619  lgsquad2  27623  2lgslem3a1  27637  2lgslem3b1  27638  2lgslem3c1  27639  2lgslem3d1  27640  2lgsoddprmlem2  27646  2sqlem3  27657  2sqlem4  27658  2sqmod  27673  chebbnd1lem2  27707  chebbnd1lem3  27708  chtppilimlem2  27711  chto1lb  27715  rplogsumlem1  27721  dchrisumlem2  27727  dchrvmasum2lem  27733  dchrisum0flblem2  27746  dchrisum0lem2a  27754  mulogsumlem  27768  mulog2sumlem2  27772  selberglem1  27782  selberg2lem  27787  selberg3lem1  27794  selberg4  27798  pntrsumo1  27802  selberg34r  27808  pntrlog2bndlem3  27816  pntrlog2bndlem4  27817  pntlemb  27834  pntlemq  27838  pntlemr  27839  pntlemj  27840  pntlemo  27844  pnt2  27850  pnt  27851  padicabvcxp  27869  ostth2lem2  27871  ostth2lem3  27872  ostth2lem4  27873  ttgcontlem1  29342  brbtwn2  29363  colinearalglem1  29364  colinearalg  29368  axpaschlem  29398  axcontlem8  29429  numclwwlk1  30842  numclwwlk7  30872  smcnlem  31179  pjhthlem1  31873  kbmul  32437  kbass2  32599  submuladdd  33213  pythagreim  33218  quad3d  33222  2exple2exp  33306  psgnfzto1st  33547  zringfrac  33966  ccfldextdgrr  34184  fldext2rspun  34194  fldext2chn  34240  constrrtlc1  34244  constrrtcclem  34246  constrrtcc  34247  constrremulcl  34279  constrmulcl  34283  cos9thpiminplylem1  34294  qqhval2lem  34493  qqhghm  34500  qqhrhm  34501  oddpwdc  34867  signsvtp  35093  signsvtn  35094  signsvfpn  35095  signsvfnn  35096  breprexplemc  35142  circlemethhgt  35153  logdivsqrle  35160  hgt750lemf  35163  hgt750lemb  35166  hgt750leme  35168  subfacval2  35768  subfaclim  35769  fwddifnp1  36747  knoppndvlem11  37221  knoppndvlem17  37227  bj-subcom  38062  bj-bary1lem1  38065  itg2addnclem  38422  itg2addnclem2  38423  itgabsnc  38440  ftc1cnnclem  38442  areacirclem1  38459  areacirc  38464  geomcau  38511  bfplem1  38574  rrndstprj2  38583  rrnequiv  38587  lcmineqlem1  42897  lcmineqlem5  42901  lcmineqlem8  42904  lcmineqlem11  42907  lcmineqlem18  42914  lcmineqlem21  42917  3lexlogpow5ineq2  42923  3lexlogpow2ineq1  42926  dvrelogpow2b  42936  aks4d1p1p7  42942  primrootscoprmpow  42967  primrootscoprbij  42970  aks6d1c1  42984  aks6d1c2  42998  2np3bcnp1  43012  2ap1caineq  43013  bcle2d  43047  aks6d1c7lem1  43048  quadfac  43073  nicomachus  43189  retire  43196  readvrec  43239  3cubeslem2  43532  3cubeslem3l  43533  3cubeslem3r  43534  irrapxlem5  43669  pellexlem2  43673  pellexlem6  43677  qirropth  43751  rmxyadd  43764  rmxm1  43777  rmxluc  43779  rmyluc2  43781  rmydbl  43783  jm2.24nn  43802  jm2.17a  43803  jm2.17b  43804  jm2.17c  43805  jm2.18  43831  jm2.19lem2  43833  jm2.22  43838  jm2.23  43839  areaquad  44059  imo72b2  45014  int-mulcomd  45018  int-rightdistd  45022  cvgdvgrat  45139  radcnvrat  45140  bccm1k  45168  binomcxplemwb  45174  binomcxplemnotnn0  45182  sineq0ALT  45761  mul13d  46115  divdiv3d  46191  mccllem  46429  coskpi2  46696  cosknegpi  46699  dvsinax  46743  dvasinbx  46750  dvcosax  46756  dvnxpaek  46772  dvnmul  46773  dvnprodlem2  46777  itgsinexplem1  46784  stoweidlem1  46831  stoweidlem11  46841  stoweidlem26  46856  stoweidlem32  46862  wallispilem4  46898  wallispi2lem1  46901  wallispi2lem2  46902  stirlinglem3  46906  stirlinglem4  46907  stirlinglem5  46908  stirlinglem7  46910  stirlinglem10  46913  stirlinglem15  46918  dirkertrigeqlem1  46928  dirkertrigeqlem2  46929  dirkertrigeqlem3  46930  dirkertrigeq  46931  dirkercncflem1  46933  fourierdlem16  46953  fourierdlem21  46958  fourierdlem22  46959  fourierdlem56  46992  fourierdlem66  47002  fourierdlem83  47019  fourierswlem  47060  fouriersw  47061  etransclem23  47087  etransclem24  47088  etransclem38  47102  etransclem46  47110  hoiprodp1  47418  hoidmvlelem2  47426  smfmullem1  47621  sigarac  47682  sigarls  47687  sigarid  47688  sigardiv  47691  sigarcol  47694  sigaradd  47696  cevathlem1  47697  sin3t  47737  cos3t  47738  sin5tlem1  47739  sin5tlem3  47741  sqrtnegnre  48197  fmtnoodd  48438  sqrtpwpw2p  48443  fmtnorec3  48453  fmtnoprmfac2lem1  48471  fmtnofac1  48475  lighneallem2  48511  lighneallem3  48512  proththd  48519  requad01  48539  dfeven2  48567  fppr2odd  48649  fpprwppr  48657  altgsumbc  49284  altgsumbcALT  49285  blennnt2  49521  dignn0flhalflem2  49548  dignn0ehalf  49549  itcovalt2lem2lem2  49606  affinecomb2  49635  rrx2linest  49674  itscnhlc0yqe  49691  itsclc0yqsollem1  49694  itscnhlc0xyqsol  49697  itschlc0xyqsol1  49698  itsclc0xyqsolr  49701  itsclquadb  49708  2itscplem3  49712  itscnhlinecirc02plem1  49714  itscnhlinecirc02plem2  49715  inlinecirc02p  49719  crosspaltd  50801  crossp3d  50802  amgmwlem  50822