Theorem mulcomd 7920

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

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136  (class class class)co 5842  ℂcc 7751   · cmul 7758

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

This theorem is referenced by:  mul31  8029  remulext2  8498  mulreim  8502  mulext2  8511  mulcanapd  8558  mulcanap2d  8559  divcanap1  8577  divrecap2  8585  div23ap  8587  divdivdivap  8609  divmuleqap  8613  divadddivap  8623  apmul2  8685  apdivmuld  8709  divcanap5rd  8714  dmdcanap2d  8717  mvllmulapd  8738  prodgt0  8747  lt2mul2div  8774  mulle0r  8839  qapne  9577  mul2lt0llt0  9697  mul2lt0lgt0  9698  mul2lt0pn  9700  modqvalr  10260  modqcyc  10294  mulp1mod1  10300  modqmul12d  10313  modqnegd  10314  modqmulmodr  10325  addmodlteq  10333  expaddzap  10499  binom2  10566  binom3  10572  bccmpl  10667  bcm1k  10673  bcn2  10677  bcpasc  10679  cvg1nlemcxze  10924  cvg1nlemcau  10926  resqrexlemcalc1  10956  resqrexlemcalc2  10957  resqrexlemnm  10960  recvalap  11039  bdtrilem  11180  reccn2ap  11254  isummulc1  11368  fsummulc1  11390  trireciplem  11441  geolim  11452  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemfm  11470  cvgratz  11473  mertensabs  11478  eftlub  11631  sinadd  11677  cosadd  11678  sin2t  11690  nndivides  11737  dvds2ln  11764  even2n  11811  oddm1even  11812  m1exp1  11838  divalgmod  11864  mulgcdr  11951  rplpwr  11960  lcmgcdlem  12009  divgcdcoprmex  12034  cncongr1  12035  oddpwdclemxy  12101  2sqpwodd  12108  eulerthlema  12162  eulerthlemth  12164  prmdiv  12167  prmdivdiv  12169  modprmn0modprm0  12188  coprimeprodsq  12189  pythagtriplem6  12202  pythagtriplem7  12203  pceulem  12226  pcadd  12271  prmpwdvds  12285  mul4sqlem  12323  evenennn  12326  dvmulxxbr  13316  dvmptcmulcn  13333  tangtx  13409  cxpmul  13483  abscxp  13485  binom4  13547  lgsdirprm  13585  lgsdi  13588  lgsdirnn0  13598  lgsdinn0  13599  2sqlem3  13603  2sqlem4  13604