Theorem mulcomd 8243

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   · cmul 8080

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

This theorem is referenced by:  mul31  8352  remulext2  8822  mulreim  8826  mulext2  8835  mulcanapd  8883  mulcanap2d  8884  divcanap1  8903  divrecap2  8911  div23ap  8913  divdivdivap  8935  divmuleqap  8939  divadddivap  8949  apmul2  9011  apdivmuld  9035  divcanap5rd  9040  dmdcanap2d  9043  mvllmulapd  9064  prodgt0  9074  lt2mul2div  9101  mulle0r  9166  subhalfhalf  9421  qapne  9917  irrmulap  9926  mul2lt0llt0  10040  mul2lt0lgt0  10041  mul2lt0pn  10043  modqvalr  10633  modqcyc  10667  mulp1mod1  10673  modqmul12d  10686  modqnegd  10687  modqmulmodr  10698  addmodlteq  10706  expaddzap  10891  binom2  10959  binom3  10965  bccmpl  11062  bcm1k  11068  bcn2  11072  bcpasc  11074  cvg1nlemcxze  11605  cvg1nlemcau  11607  resqrexlemcalc1  11637  resqrexlemcalc2  11638  resqrexlemnm  11641  recvalap  11720  bdtrilem  11862  reccn2ap  11936  isummulc1  12051  fsummulc1  12073  trireciplem  12124  geolim  12135  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemfm  12153  cvgratz  12156  mertensabs  12161  eftlub  12314  sinadd  12360  cosadd  12361  sin2t  12373  nndivides  12421  dvds2ln  12448  even2n  12498  oddm1even  12499  m1exp1  12525  divalgmod  12551  bitsp1  12575  bitsinv1lem  12585  mulgcdr  12652  rplpwr  12661  lcmgcdlem  12712  divgcdcoprmex  12737  cncongr1  12738  oddpwdclemxy  12804  2sqpwodd  12811  eulerthlema  12865  eulerthlemth  12867  prmdiv  12870  prmdivdiv  12872  modprmn0modprm0  12892  coprimeprodsq  12893  pythagtriplem6  12906  pythagtriplem7  12907  pceulem  12930  pcadd  12976  prmpwdvds  12991  mul4sqlem  13029  4sqlem17  13043  evenennn  13077  mulgassr  13810  znunit  14738  dvmulxxbr  15496  dvmptcmulcn  15515  dvply1  15559  tangtx  15632  cxpmul  15706  abscxp  15709  binom4  15773  pellexlem2  15775  wilthlem1  15777  mpodvdsmulf1o  15787  sgmppw  15789  perfect1  15795  lgsdirprm  15836  lgsdi  15839  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem1a  15860  gausslemma2dlem6  15869  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2  15885  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgslem3d1  15902  2lgsoddprmlem2  15908  2sqlem3  15919  2sqlem4  15920