Theorem mulcomd 8043

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   · cmul 7879

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

This theorem is referenced by:  mul31  8152  remulext2  8621  mulreim  8625  mulext2  8634  mulcanapd  8682  mulcanap2d  8683  divcanap1  8702  divrecap2  8710  div23ap  8712  divdivdivap  8734  divmuleqap  8738  divadddivap  8748  apmul2  8810  apdivmuld  8834  divcanap5rd  8839  dmdcanap2d  8842  mvllmulapd  8863  prodgt0  8873  lt2mul2div  8900  mulle0r  8965  subhalfhalf  9220  qapne  9707  irrmulap  9716  mul2lt0llt0  9830  mul2lt0lgt0  9831  mul2lt0pn  9833  modqvalr  10399  modqcyc  10433  mulp1mod1  10439  modqmul12d  10452  modqnegd  10453  modqmulmodr  10464  addmodlteq  10472  expaddzap  10657  binom2  10725  binom3  10731  bccmpl  10828  bcm1k  10834  bcn2  10838  bcpasc  10840  cvg1nlemcxze  11129  cvg1nlemcau  11131  resqrexlemcalc1  11161  resqrexlemcalc2  11162  resqrexlemnm  11165  recvalap  11244  bdtrilem  11385  reccn2ap  11459  isummulc1  11573  fsummulc1  11595  trireciplem  11646  geolim  11657  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratnnlemfm  11675  cvgratz  11678  mertensabs  11683  eftlub  11836  sinadd  11882  cosadd  11883  sin2t  11895  nndivides  11943  dvds2ln  11970  even2n  12018  oddm1even  12019  m1exp1  12045  divalgmod  12071  mulgcdr  12158  rplpwr  12167  lcmgcdlem  12218  divgcdcoprmex  12243  cncongr1  12244  oddpwdclemxy  12310  2sqpwodd  12317  eulerthlema  12371  eulerthlemth  12373  prmdiv  12376  prmdivdiv  12378  modprmn0modprm0  12397  coprimeprodsq  12398  pythagtriplem6  12411  pythagtriplem7  12412  pceulem  12435  pcadd  12481  prmpwdvds  12496  mul4sqlem  12534  4sqlem17  12548  evenennn  12553  mulgassr  13233  znunit  14158  dvmulxxbr  14881  dvmptcmulcn  14900  dvply1  14943  tangtx  15014  cxpmul  15088  abscxp  15090  binom4  15152  wilthlem1  15153  lgsdirprm  15191  lgsdi  15194  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem1a  15215  gausslemma2dlem6  15224  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2  15240  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  2lgsoddprmlem2  15263  2sqlem3  15274  2sqlem4  15275