Theorem mulcomd 11229

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  (class class class)co 7410  ℂcc 11097   · cmul 11104

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  mul31  11376  mul4r  11378  mulcand  11846  mulcan2d  11847  divcan1  11880  divrec2  11888  div23  11890  muldivdid  11908  divdivdiv  11915  divmuleq  11919  divadddiv  11929  divcan5rd  12017  dmdcan2d  12020  mvllmuld  12046  rdiv  12049  subhalfhalf  12477  mul2lt0llt0  13121  mul2lt0lgt0  13122  prodge0ld  13125  xmulcom  13291  modvalr  13905  mulp1mod1  13947  modmul12d  13961  modnegd  13962  modmulmodr  13973  expaddz  14142  binom3  14260  expmulnbnd  14271  digit1  14273  bccmpl  14345  bcm1k  14351  bcn2  14355  bcpasc  14357  sgnmul  15144  recval  15374  abs1m  15387  bhmafibid1cn  15517  bhmafibid2cn  15518  reccn2  15648  lo1mul2  15680  isummulc1  15814  fsummulc1  15836  incexclem  15890  incexc  15891  trireciplem  15916  pwdif  15922  geolim  15924  cvgrat  15937  mertens  15940  ntrivcvgmul  15956  fallfacfwd  16089  bpoly4  16112  fsumcube  16113  eftlub  16164  sinadd  16219  cosadd  16220  sin2t  16232  nndivides  16319  dvds2ln  16346  even2n  16399  oddm1even  16400  mod2eq1n2dvds  16404  m1exp1  16433  pwp1fsum  16448  divalgmod  16463  bitsp1  16488  bitsinv1lem  16498  sadadd2lem  16516  smumullem  16549  gcdmultiplez  16592  mulgcdr  16607  rplpwr  16615  lcmgcdlem  16663  divgcdcoprmex  16723  cncongr1  16724  eulerthlem2  16840  prmdiv  16843  prmdivdiv  16845  vfermltlALT  16861  modprmn0modprm0  16866  coprimeprodsq  16867  pythagtriplem6  16880  pythagtriplem7  16881  pceulem  16904  pcadd  16948  prmpwdvds  16963  mul4sqlem  17012  4sqlem17  17020  mulgassr  19177  odmodnn0  19609  odmulg  19625  odmulgeq  19626  odbezout  19627  odadd1  19917  ablfacrp2  20138  pgpfac1lem3  20148  zringlpirlem3  21593  znunit  21692  icopnfhmeo  25081  cphassr  25350  pjthlem1  25575  itgabs  25973  dvmulbr  26077  dvcmul  26082  dvcmulf  26083  dvmptcmul  26102  cmvth  26129  dvlipcn  26132  c1liplem1  26134  lhop1lem  26151  lhop2  26153  dvcvx  26158  dvfsumlem2  26165  ftc1lem4  26177  itgparts  26185  plyn0mulidp  26421  dvply1  26424  elqaalem3  26461  aalioulem4  26475  taylthlem2  26513  abelthlem6  26575  abelthlem7  26577  tangtx  26646  tanarg  26760  advlogexp  26796  mulcxp  26826  cxpmul  26829  abscxp  26833  dvcxp2  26882  cxpeq  26898  ang180lem1  26950  lawcoslem1  26956  lawcos  26957  heron  26979  dcubic1  26986  mcubic  26988  cubic2  26989  binom4  26991  dquart  26994  quart1lem  26996  quart1  26997  quartlem1  26998  dvatan  27076  leibpi  27083  log2cnv  27085  efrlim  27110  cxp2lim  27117  cxploglim  27118  zetacvg  27155  lgamgulmlem2  27170  lgamgulmlem3  27171  wilthlem1  27208  ftalem1  27213  ftalem5  27217  basellem3  27223  basellem5  27225  mpodvdsmulf1o  27334  dvdsmulf1o  27336  sgmppw  27337  logfac2  27357  chpval2  27358  chpchtsum  27359  perfect1  27368  lgsdirprm  27471  lgsdi  27474  lgsdirnn0  27484  lgsdinn0  27485  gausslemma2dlem1a  27505  gausslemma2dlem6  27512  lgsquadlem1  27520  lgsquadlem2  27521  lgsquadlem3  27522  lgsquad2  27526  2lgslem3a1  27540  2lgslem3b1  27541  2lgslem3c1  27542  2lgslem3d1  27543  2lgsoddprmlem2  27549  2sqlem3  27560  2sqlem4  27561  2sqmod  27576  chebbnd1lem2  27610  chebbnd1lem3  27611  chtppilimlem2  27614  chto1lb  27618  rplogsumlem1  27624  dchrisumlem2  27630  dchrvmasum2lem  27636  dchrisum0flblem2  27649  dchrisum0lem2a  27657  mulogsumlem  27671  mulog2sumlem2  27675  selberglem1  27685  selberg2lem  27690  selberg3lem1  27697  selberg4  27701  pntrsumo1  27705  selberg34r  27711  pntrlog2bndlem3  27719  pntrlog2bndlem4  27720  pntlemb  27737  pntlemq  27741  pntlemr  27742  pntlemj  27743  pntlemo  27747  pnt2  27753  pnt  27754  padicabvcxp  27772  ostth2lem2  27774  ostth2lem3  27775  ostth2lem4  27776  ttgcontlem1  29200  brbtwn2  29221  colinearalglem1  29222  colinearalg  29226  axpaschlem  29256  axcontlem8  29287  numclwwlk1  30678  numclwwlk7  30708  smcnlem  31015  pjhthlem1  31709  kbmul  32273  kbass2  32435  submuladdd  33051  pythagreim  33056  quad3d  33060  2exple2exp  33144  psgnfzto1st  33391  zringfrac  33810  ccfldextdgrr  34028  fldext2rspun  34038  fldext2chn  34084  constrrtlc1  34088  constrrtcclem  34090  constrrtcc  34091  constrremulcl  34123  constrmulcl  34127  cos9thpiminplylem1  34138  qqhval2lem  34337  qqhghm  34344  qqhrhm  34345  oddpwdc  34710  signsvtp  34936  signsvtn  34937  signsvfpn  34938  signsvfnn  34939  breprexplemc  34985  circlemethhgt  34996  logdivsqrle  35003  hgt750lemf  35006  hgt750lemb  35009  hgt750leme  35011  subfacval2  35645  subfaclim  35646  fwddifnp1  36623  knoppndvlem11  37077  knoppndvlem17  37083  bj-subcom  37918  bj-bary1lem1  37921  itg2addnclem  38288  itg2addnclem2  38289  itgabsnc  38306  ftc1cnnclem  38308  areacirclem1  38325  areacirc  38330  geomcau  38376  bfplem1  38439  rrndstprj2  38448  rrnequiv  38452  lcmineqlem1  42764  lcmineqlem5  42768  lcmineqlem8  42771  lcmineqlem11  42774  lcmineqlem18  42781  lcmineqlem21  42784  3lexlogpow5ineq2  42790  3lexlogpow2ineq1  42793  dvrelogpow2b  42803  aks4d1p1p7  42809  primrootscoprmpow  42834  primrootscoprbij  42837  aks6d1c1  42851  aks6d1c2  42865  2np3bcnp1  42879  2ap1caineq  42880  bcle2d  42914  aks6d1c7lem1  42915  quadfac  42940  nicomachus  43041  retire  43048  readvrec  43091  3cubeslem2  43386  3cubeslem3l  43387  3cubeslem3r  43388  irrapxlem5  43523  pellexlem2  43527  pellexlem6  43531  qirropth  43605  rmxyadd  43618  rmxm1  43631  rmxluc  43633  rmyluc2  43635  rmydbl  43637  jm2.24nn  43656  jm2.17a  43657  jm2.17b  43658  jm2.17c  43659  jm2.18  43685  jm2.19lem2  43687  jm2.22  43692  jm2.23  43693  areaquad  43913  imo72b2  44868  int-mulcomd  44872  int-rightdistd  44876  cvgdvgrat  44993  radcnvrat  44994  bccm1k  45022  binomcxplemwb  45028  binomcxplemnotnn0  45036  sineq0ALT  45615  mul13d  45969  divdiv3d  46045  mccllem  46283  coskpi2  46550  cosknegpi  46553  dvsinax  46597  dvasinbx  46604  dvcosax  46610  dvnxpaek  46626  dvnmul  46627  dvnprodlem2  46631  itgsinexplem1  46638  stoweidlem1  46685  stoweidlem11  46695  stoweidlem26  46710  stoweidlem32  46716  wallispilem4  46752  wallispi2lem1  46755  wallispi2lem2  46756  stirlinglem3  46760  stirlinglem4  46761  stirlinglem5  46762  stirlinglem7  46764  stirlinglem10  46767  stirlinglem15  46772  dirkertrigeqlem1  46782  dirkertrigeqlem2  46783  dirkertrigeqlem3  46784  dirkertrigeq  46785  dirkercncflem1  46787  fourierdlem16  46807  fourierdlem21  46812  fourierdlem22  46813  fourierdlem56  46846  fourierdlem66  46856  fourierdlem83  46873  fourierswlem  46914  fouriersw  46915  etransclem23  46941  etransclem24  46942  etransclem38  46956  etransclem46  46964  hoiprodp1  47272  hoidmvlelem2  47280  smfmullem1  47475  sigarac  47536  sigarls  47541  sigarid  47542  sigardiv  47545  sigarcol  47548  sigaradd  47550  cevathlem1  47551  sin3t  47575  cos3t  47576  sin5tlem1  47577  sin5tlem3  47579  sqrtnegnre  48011  fmtnoodd  48252  sqrtpwpw2p  48257  fmtnorec3  48267  fmtnoprmfac2lem1  48285  fmtnofac1  48289  lighneallem2  48325  lighneallem3  48326  proththd  48333  requad01  48353  dfeven2  48381  fppr2odd  48463  fpprwppr  48471  altgsumbc  49099  altgsumbcALT  49100  blennnt2  49336  dignn0flhalflem2  49363  dignn0ehalf  49364  itcovalt2lem2lem2  49421  affinecomb2  49450  rrx2linest  49489  itscnhlc0yqe  49506  itsclc0yqsollem1  49509  itscnhlc0xyqsol  49512  itschlc0xyqsol1  49513  itsclc0xyqsolr  49516  itsclquadb  49523  2itscplem3  49527  itscnhlinecirc02plem1  49529  itscnhlinecirc02plem2  49530  inlinecirc02p  49534  amgmwlem  50569