Theorem mulcomd 8176

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   · cmul 8012

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

This theorem is referenced by:  mul31  8285  remulext2  8755  mulreim  8759  mulext2  8768  mulcanapd  8816  mulcanap2d  8817  divcanap1  8836  divrecap2  8844  div23ap  8846  divdivdivap  8868  divmuleqap  8872  divadddivap  8882  apmul2  8944  apdivmuld  8968  divcanap5rd  8973  dmdcanap2d  8976  mvllmulapd  8997  prodgt0  9007  lt2mul2div  9034  mulle0r  9099  subhalfhalf  9354  qapne  9842  irrmulap  9851  mul2lt0llt0  9965  mul2lt0lgt0  9966  mul2lt0pn  9968  modqvalr  10555  modqcyc  10589  mulp1mod1  10595  modqmul12d  10608  modqnegd  10609  modqmulmodr  10620  addmodlteq  10628  expaddzap  10813  binom2  10881  binom3  10887  bccmpl  10984  bcm1k  10990  bcn2  10994  bcpasc  10996  cvg1nlemcxze  11501  cvg1nlemcau  11503  resqrexlemcalc1  11533  resqrexlemcalc2  11534  resqrexlemnm  11537  recvalap  11616  bdtrilem  11758  reccn2ap  11832  isummulc1  11946  fsummulc1  11968  trireciplem  12019  geolim  12030  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  cvgratnnlemfm  12048  cvgratz  12051  mertensabs  12056  eftlub  12209  sinadd  12255  cosadd  12256  sin2t  12268  nndivides  12316  dvds2ln  12343  even2n  12393  oddm1even  12394  m1exp1  12420  divalgmod  12446  bitsp1  12470  bitsinv1lem  12480  mulgcdr  12547  rplpwr  12556  lcmgcdlem  12607  divgcdcoprmex  12632  cncongr1  12633  oddpwdclemxy  12699  2sqpwodd  12706  eulerthlema  12760  eulerthlemth  12762  prmdiv  12765  prmdivdiv  12767  modprmn0modprm0  12787  coprimeprodsq  12788  pythagtriplem6  12801  pythagtriplem7  12802  pceulem  12825  pcadd  12871  prmpwdvds  12886  mul4sqlem  12924  4sqlem17  12938  evenennn  12972  mulgassr  13705  znunit  14631  dvmulxxbr  15384  dvmptcmulcn  15403  dvply1  15447  tangtx  15520  cxpmul  15594  abscxp  15597  binom4  15661  wilthlem1  15662  mpodvdsmulf1o  15672  sgmppw  15674  perfect1  15680  lgsdirprm  15721  lgsdi  15724  lgsdirnn0  15734  lgsdinn0  15735  gausslemma2dlem1a  15745  gausslemma2dlem6  15754  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2  15770  2lgslem3a1  15784  2lgslem3b1  15785  2lgslem3c1  15786  2lgslem3d1  15787  2lgsoddprmlem2  15793  2sqlem3  15804  2sqlem4  15805