Theorem mulcomd 7953

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2146  (class class class)co 5865  ℂcc 7784   · cmul 7791

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

This theorem is referenced by:  mul31  8062  remulext2  8531  mulreim  8535  mulext2  8544  mulcanapd  8591  mulcanap2d  8592  divcanap1  8611  divrecap2  8619  div23ap  8621  divdivdivap  8643  divmuleqap  8647  divadddivap  8657  apmul2  8719  apdivmuld  8743  divcanap5rd  8748  dmdcanap2d  8751  mvllmulapd  8772  prodgt0  8782  lt2mul2div  8809  mulle0r  8874  qapne  9612  mul2lt0llt0  9732  mul2lt0lgt0  9733  mul2lt0pn  9735  modqvalr  10295  modqcyc  10329  mulp1mod1  10335  modqmul12d  10348  modqnegd  10349  modqmulmodr  10360  addmodlteq  10368  expaddzap  10534  binom2  10601  binom3  10607  bccmpl  10702  bcm1k  10708  bcn2  10712  bcpasc  10714  cvg1nlemcxze  10959  cvg1nlemcau  10961  resqrexlemcalc1  10991  resqrexlemcalc2  10992  resqrexlemnm  10995  recvalap  11074  bdtrilem  11215  reccn2ap  11289  isummulc1  11403  fsummulc1  11425  trireciplem  11476  geolim  11487  cvgratnnlemnexp  11500  cvgratnnlemmn  11501  cvgratnnlemfm  11505  cvgratz  11508  mertensabs  11513  eftlub  11666  sinadd  11712  cosadd  11713  sin2t  11725  nndivides  11772  dvds2ln  11799  even2n  11846  oddm1even  11847  m1exp1  11873  divalgmod  11899  mulgcdr  11986  rplpwr  11995  lcmgcdlem  12044  divgcdcoprmex  12069  cncongr1  12070  oddpwdclemxy  12136  2sqpwodd  12143  eulerthlema  12197  eulerthlemth  12199  prmdiv  12202  prmdivdiv  12204  modprmn0modprm0  12223  coprimeprodsq  12224  pythagtriplem6  12237  pythagtriplem7  12238  pceulem  12261  pcadd  12306  prmpwdvds  12320  mul4sqlem  12358  evenennn  12361  mulgassr  12881  dvmulxxbr  13737  dvmptcmulcn  13754  tangtx  13830  cxpmul  13904  abscxp  13906  binom4  13968  lgsdirprm  14006  lgsdi  14009  lgsdirnn0  14019  lgsdinn0  14020  2sqlem3  14024  2sqlem4  14025