Theorem mulcomd 8009

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2160  (class class class)co 5896  ℂcc 7839   · cmul 7846

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

This theorem is referenced by:  mul31  8118  remulext2  8587  mulreim  8591  mulext2  8600  mulcanapd  8648  mulcanap2d  8649  divcanap1  8668  divrecap2  8676  div23ap  8678  divdivdivap  8700  divmuleqap  8704  divadddivap  8714  apmul2  8776  apdivmuld  8800  divcanap5rd  8805  dmdcanap2d  8808  mvllmulapd  8829  prodgt0  8839  lt2mul2div  8866  mulle0r  8931  qapne  9669  mul2lt0llt0  9791  mul2lt0lgt0  9792  mul2lt0pn  9794  modqvalr  10356  modqcyc  10390  mulp1mod1  10396  modqmul12d  10409  modqnegd  10410  modqmulmodr  10421  addmodlteq  10429  expaddzap  10595  binom2  10663  binom3  10669  bccmpl  10766  bcm1k  10772  bcn2  10776  bcpasc  10778  cvg1nlemcxze  11023  cvg1nlemcau  11025  resqrexlemcalc1  11055  resqrexlemcalc2  11056  resqrexlemnm  11059  recvalap  11138  bdtrilem  11279  reccn2ap  11353  isummulc1  11467  fsummulc1  11489  trireciplem  11540  geolim  11551  cvgratnnlemnexp  11564  cvgratnnlemmn  11565  cvgratnnlemfm  11569  cvgratz  11572  mertensabs  11577  eftlub  11730  sinadd  11776  cosadd  11777  sin2t  11789  nndivides  11836  dvds2ln  11863  even2n  11911  oddm1even  11912  m1exp1  11938  divalgmod  11964  mulgcdr  12051  rplpwr  12060  lcmgcdlem  12109  divgcdcoprmex  12134  cncongr1  12135  oddpwdclemxy  12201  2sqpwodd  12208  eulerthlema  12262  eulerthlemth  12264  prmdiv  12267  prmdivdiv  12269  modprmn0modprm0  12288  coprimeprodsq  12289  pythagtriplem6  12302  pythagtriplem7  12303  pceulem  12326  pcadd  12372  prmpwdvds  12387  mul4sqlem  12425  4sqlem17  12439  evenennn  12444  mulgassr  13100  dvmulxxbr  14623  dvmptcmulcn  14640  tangtx  14716  cxpmul  14790  abscxp  14792  binom4  14854  wilthlem1  14855  lgsdirprm  14893  lgsdi  14896  lgsdirnn0  14906  lgsdinn0  14907  2lgsoddprmlem2  14912  2sqlem3  14922  2sqlem4  14923