Theorem mulcomd 8041

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   · cmul 7877

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

This theorem is referenced by:  mul31  8150  remulext2  8619  mulreim  8623  mulext2  8632  mulcanapd  8680  mulcanap2d  8681  divcanap1  8700  divrecap2  8708  div23ap  8710  divdivdivap  8732  divmuleqap  8736  divadddivap  8746  apmul2  8808  apdivmuld  8832  divcanap5rd  8837  dmdcanap2d  8840  mvllmulapd  8861  prodgt0  8871  lt2mul2div  8898  mulle0r  8963  subhalfhalf  9217  qapne  9704  irrmulap  9713  mul2lt0llt0  9827  mul2lt0lgt0  9828  mul2lt0pn  9830  modqvalr  10396  modqcyc  10430  mulp1mod1  10436  modqmul12d  10449  modqnegd  10450  modqmulmodr  10461  addmodlteq  10469  expaddzap  10654  binom2  10722  binom3  10728  bccmpl  10825  bcm1k  10831  bcn2  10835  bcpasc  10837  cvg1nlemcxze  11126  cvg1nlemcau  11128  resqrexlemcalc1  11158  resqrexlemcalc2  11159  resqrexlemnm  11162  recvalap  11241  bdtrilem  11382  reccn2ap  11456  isummulc1  11570  fsummulc1  11592  trireciplem  11643  geolim  11654  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemfm  11672  cvgratz  11675  mertensabs  11680  eftlub  11833  sinadd  11879  cosadd  11880  sin2t  11892  nndivides  11940  dvds2ln  11967  even2n  12015  oddm1even  12016  m1exp1  12042  divalgmod  12068  mulgcdr  12155  rplpwr  12164  lcmgcdlem  12215  divgcdcoprmex  12240  cncongr1  12241  oddpwdclemxy  12307  2sqpwodd  12314  eulerthlema  12368  eulerthlemth  12370  prmdiv  12373  prmdivdiv  12375  modprmn0modprm0  12394  coprimeprodsq  12395  pythagtriplem6  12408  pythagtriplem7  12409  pceulem  12432  pcadd  12478  prmpwdvds  12493  mul4sqlem  12531  4sqlem17  12545  evenennn  12550  mulgassr  13230  znunit  14147  dvmulxxbr  14851  dvmptcmulcn  14868  tangtx  14973  cxpmul  15047  abscxp  15049  binom4  15111  wilthlem1  15112  lgsdirprm  15150  lgsdi  15153  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1a  15174  gausslemma2dlem6  15183  lgsquadlem1  15191  2lgsoddprmlem2  15194  2sqlem3  15204  2sqlem4  15205