Theorem mulcomd 8048

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   · cmul 7884

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

This theorem is referenced by:  mul31  8157  remulext2  8627  mulreim  8631  mulext2  8640  mulcanapd  8688  mulcanap2d  8689  divcanap1  8708  divrecap2  8716  div23ap  8718  divdivdivap  8740  divmuleqap  8744  divadddivap  8754  apmul2  8816  apdivmuld  8840  divcanap5rd  8845  dmdcanap2d  8848  mvllmulapd  8869  prodgt0  8879  lt2mul2div  8906  mulle0r  8971  subhalfhalf  9226  qapne  9713  irrmulap  9722  mul2lt0llt0  9836  mul2lt0lgt0  9837  mul2lt0pn  9839  modqvalr  10417  modqcyc  10451  mulp1mod1  10457  modqmul12d  10470  modqnegd  10471  modqmulmodr  10482  addmodlteq  10490  expaddzap  10675  binom2  10743  binom3  10749  bccmpl  10846  bcm1k  10852  bcn2  10856  bcpasc  10858  cvg1nlemcxze  11147  cvg1nlemcau  11149  resqrexlemcalc1  11179  resqrexlemcalc2  11180  resqrexlemnm  11183  recvalap  11262  bdtrilem  11404  reccn2ap  11478  isummulc1  11592  fsummulc1  11614  trireciplem  11665  geolim  11676  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemfm  11694  cvgratz  11697  mertensabs  11702  eftlub  11855  sinadd  11901  cosadd  11902  sin2t  11914  nndivides  11962  dvds2ln  11989  even2n  12039  oddm1even  12040  m1exp1  12066  divalgmod  12092  bitsp1  12115  mulgcdr  12185  rplpwr  12194  lcmgcdlem  12245  divgcdcoprmex  12270  cncongr1  12271  oddpwdclemxy  12337  2sqpwodd  12344  eulerthlema  12398  eulerthlemth  12400  prmdiv  12403  prmdivdiv  12405  modprmn0modprm0  12425  coprimeprodsq  12426  pythagtriplem6  12439  pythagtriplem7  12440  pceulem  12463  pcadd  12509  prmpwdvds  12524  mul4sqlem  12562  4sqlem17  12576  evenennn  12610  mulgassr  13290  znunit  14215  dvmulxxbr  14938  dvmptcmulcn  14957  dvply1  15001  tangtx  15074  cxpmul  15148  abscxp  15151  binom4  15215  wilthlem1  15216  mpodvdsmulf1o  15226  sgmppw  15228  perfect1  15234  lgsdirprm  15275  lgsdi  15278  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1a  15299  gausslemma2dlem6  15308  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2  15324  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  2lgsoddprmlem2  15347  2sqlem3  15358  2sqlem4  15359