Theorem mulcomd 8101

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930   · cmul 7937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcom 8033

This theorem is referenced by:  mul31  8210  remulext2  8680  mulreim  8684  mulext2  8693  mulcanapd  8741  mulcanap2d  8742  divcanap1  8761  divrecap2  8769  div23ap  8771  divdivdivap  8793  divmuleqap  8797  divadddivap  8807  apmul2  8869  apdivmuld  8893  divcanap5rd  8898  dmdcanap2d  8901  mvllmulapd  8922  prodgt0  8932  lt2mul2div  8959  mulle0r  9024  subhalfhalf  9279  qapne  9767  irrmulap  9776  mul2lt0llt0  9890  mul2lt0lgt0  9891  mul2lt0pn  9893  modqvalr  10477  modqcyc  10511  mulp1mod1  10517  modqmul12d  10530  modqnegd  10531  modqmulmodr  10542  addmodlteq  10550  expaddzap  10735  binom2  10803  binom3  10809  bccmpl  10906  bcm1k  10912  bcn2  10916  bcpasc  10918  cvg1nlemcxze  11337  cvg1nlemcau  11339  resqrexlemcalc1  11369  resqrexlemcalc2  11370  resqrexlemnm  11373  recvalap  11452  bdtrilem  11594  reccn2ap  11668  isummulc1  11782  fsummulc1  11804  trireciplem  11855  geolim  11866  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  cvgratnnlemfm  11884  cvgratz  11887  mertensabs  11892  eftlub  12045  sinadd  12091  cosadd  12092  sin2t  12104  nndivides  12152  dvds2ln  12179  even2n  12229  oddm1even  12230  m1exp1  12256  divalgmod  12282  bitsp1  12306  bitsinv1lem  12316  mulgcdr  12383  rplpwr  12392  lcmgcdlem  12443  divgcdcoprmex  12468  cncongr1  12469  oddpwdclemxy  12535  2sqpwodd  12542  eulerthlema  12596  eulerthlemth  12598  prmdiv  12601  prmdivdiv  12603  modprmn0modprm0  12623  coprimeprodsq  12624  pythagtriplem6  12637  pythagtriplem7  12638  pceulem  12661  pcadd  12707  prmpwdvds  12722  mul4sqlem  12760  4sqlem17  12774  evenennn  12808  mulgassr  13540  znunit  14465  dvmulxxbr  15218  dvmptcmulcn  15237  dvply1  15281  tangtx  15354  cxpmul  15428  abscxp  15431  binom4  15495  wilthlem1  15496  mpodvdsmulf1o  15506  sgmppw  15508  perfect1  15514  lgsdirprm  15555  lgsdi  15558  lgsdirnn0  15568  lgsdinn0  15569  gausslemma2dlem1a  15579  gausslemma2dlem6  15588  lgsquadlem1  15598  lgsquadlem2  15599  lgsquadlem3  15600  lgsquad2  15604  2lgslem3a1  15618  2lgslem3b1  15619  2lgslem3c1  15620  2lgslem3d1  15621  2lgsoddprmlem2  15627  2sqlem3  15638  2sqlem4  15639