Theorem mulcomd 8184

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   · cmul 8020

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

This theorem is referenced by:  mul31  8293  remulext2  8763  mulreim  8767  mulext2  8776  mulcanapd  8824  mulcanap2d  8825  divcanap1  8844  divrecap2  8852  div23ap  8854  divdivdivap  8876  divmuleqap  8880  divadddivap  8890  apmul2  8952  apdivmuld  8976  divcanap5rd  8981  dmdcanap2d  8984  mvllmulapd  9005  prodgt0  9015  lt2mul2div  9042  mulle0r  9107  subhalfhalf  9362  qapne  9851  irrmulap  9860  mul2lt0llt0  9974  mul2lt0lgt0  9975  mul2lt0pn  9977  modqvalr  10564  modqcyc  10598  mulp1mod1  10604  modqmul12d  10617  modqnegd  10618  modqmulmodr  10629  addmodlteq  10637  expaddzap  10822  binom2  10890  binom3  10896  bccmpl  10993  bcm1k  10999  bcn2  11003  bcpasc  11005  cvg1nlemcxze  11514  cvg1nlemcau  11516  resqrexlemcalc1  11546  resqrexlemcalc2  11547  resqrexlemnm  11550  recvalap  11629  bdtrilem  11771  reccn2ap  11845  isummulc1  11959  fsummulc1  11981  trireciplem  12032  geolim  12043  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  cvgratnnlemfm  12061  cvgratz  12064  mertensabs  12069  eftlub  12222  sinadd  12268  cosadd  12269  sin2t  12281  nndivides  12329  dvds2ln  12356  even2n  12406  oddm1even  12407  m1exp1  12433  divalgmod  12459  bitsp1  12483  bitsinv1lem  12493  mulgcdr  12560  rplpwr  12569  lcmgcdlem  12620  divgcdcoprmex  12645  cncongr1  12646  oddpwdclemxy  12712  2sqpwodd  12719  eulerthlema  12773  eulerthlemth  12775  prmdiv  12778  prmdivdiv  12780  modprmn0modprm0  12800  coprimeprodsq  12801  pythagtriplem6  12814  pythagtriplem7  12815  pceulem  12838  pcadd  12884  prmpwdvds  12899  mul4sqlem  12937  4sqlem17  12951  evenennn  12985  mulgassr  13718  znunit  14644  dvmulxxbr  15397  dvmptcmulcn  15416  dvply1  15460  tangtx  15533  cxpmul  15607  abscxp  15610  binom4  15674  wilthlem1  15675  mpodvdsmulf1o  15685  sgmppw  15687  perfect1  15693  lgsdirprm  15734  lgsdi  15737  lgsdirnn0  15747  lgsdinn0  15748  gausslemma2dlem1a  15758  gausslemma2dlem6  15767  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad2  15783  2lgslem3a1  15797  2lgslem3b1  15798  2lgslem3c1  15799  2lgslem3d1  15800  2lgsoddprmlem2  15806  2sqlem3  15817  2sqlem4  15818