Theorem mulcomd 8300

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130   · cmul 8137

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

This theorem is referenced by:  mul31  8409  remulext2  8879  mulreim  8883  mulext2  8892  mulcanapd  8940  mulcanap2d  8941  divcanap1  8960  divrecap2  8968  div23ap  8970  divdivdivap  8992  divmuleqap  8996  divadddivap  9006  apmul2  9068  apdivmuld  9092  divcanap5rd  9097  dmdcanap2d  9100  mvllmulapd  9121  prodgt0  9131  lt2mul2div  9158  mulle0r  9223  subhalfhalf  9478  qapne  9977  irrmulap  9986  mul2lt0llt0  10100  mul2lt0lgt0  10101  mul2lt0pn  10103  modqvalr  10694  modqcyc  10728  mulp1mod1  10734  modqmul12d  10747  modqnegd  10748  modqmulmodr  10759  addmodlteq  10767  expaddzap  10952  binom2  11020  binom3  11026  bccmpl  11124  bcm1k  11130  bcn2  11134  bcpasc  11136  cvg1nlemcxze  11675  cvg1nlemcau  11677  resqrexlemcalc1  11707  resqrexlemcalc2  11708  resqrexlemnm  11711  recvalap  11790  bdtrilem  11932  reccn2ap  12006  isummulc1  12121  fsummulc1  12143  trireciplem  12194  geolim  12205  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  cvgratnnlemfm  12223  cvgratz  12226  mertensabs  12231  eftlub  12384  sinadd  12430  cosadd  12431  sin2t  12443  nndivides  12491  dvds2ln  12518  even2n  12568  oddm1even  12569  m1exp1  12595  divalgmod  12621  bitsp1  12645  bitsinv1lem  12655  mulgcdr  12722  rplpwr  12731  lcmgcdlem  12782  divgcdcoprmex  12807  cncongr1  12808  oddpwdclemxy  12874  2sqpwodd  12881  eulerthlema  12935  eulerthlemth  12937  prmdiv  12940  prmdivdiv  12942  modprmn0modprm0  12962  coprimeprodsq  12963  pythagtriplem6  12976  pythagtriplem7  12977  pceulem  13000  pcadd  13046  prmpwdvds  13061  mul4sqlem  13099  4sqlem17  13113  evenennn  13165  mulgassr  13898  znunit  14856  dvmulxxbr  15616  dvmptcmulcn  15635  dvply1  15679  tangtx  15752  cxpmul  15826  abscxp  15829  binom4  15893  pellexlem2  15895  wilthlem1  15897  mpodvdsmulf1o  15907  sgmppw  15909  perfect1  15915  lgsdirprm  15956  lgsdi  15959  lgsdirnn0  15969  lgsdinn0  15970  gausslemma2dlem1a  15980  gausslemma2dlem6  15989  lgsquadlem1  15999  lgsquadlem2  16000  lgsquadlem3  16001  lgsquad2  16005  2lgslem3a1  16019  2lgslem3b1  16020  2lgslem3c1  16021  2lgslem3d1  16022  2lgsoddprmlem2  16028  2sqlem3  16039  2sqlem4  16040