Theorem mul12d 11427

Description: Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcomd.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addcand.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
mul12d	⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))

Proof of Theorem mul12d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcomd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcand.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		mul12 11383	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1371	1 ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7411  ℂcc 11110   · cmul 11117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-mulcom 11176  ax-mulass 11178

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414

This theorem is referenced by:  divrec  11892  remullem  15079  sqreulem  15310  cvgrat  15833  binomrisefac  15990  tanval3  16081  sinadd  16111  dvdsmulgcd  16501  lcmgcdlem  16547  cncongr1  16608  prmdiv  16722  vdwlem6  16923  itgmulc2  25575  dvexp3  25719  aaliou3lem8  26082  dvradcnv  26157  pserdvlem2  26164  abelthlem6  26172  abelthlem7  26174  tangtx  26239  tanarg  26351  dvcxp1  26472  dvcncxp1  26475  heron  26567  dcubic1  26574  mcubic  26576  dquart  26582  quart1  26585  quartlem1  26586  asinsin  26621  lgamgulmlem2  26758  basellem3  26811  bcp1ctr  27006  gausslemma2dlem6  27099  lgseisenlem2  27103  lgseisenlem4  27105  lgsquadlem1  27107  2sqlem4  27148  chebbnd1lem3  27198  rpvmasum2  27239  mulog2sumlem3  27263  selberglem1  27272  selberg4lem1  27287  selberg3r  27296  selberg34r  27298  pntrlog2bndlem4  27307  pntrlog2bndlem6  27310  pntlemr  27329  pntlemk  27333  ostth2lem3  27362  colinearalglem4  28422  branmfn  31613  vtsprod  33937  hgt750leme  33956  faclimlem1  35005  itgmulc2nc  36859  areacirclem1  36879  3factsumint2  41193  lcmineqlem10  41209  lcmineqlem11  41210  pellexlem6  41874  pell1234qrmulcl  41895  rmxyadd  41962  jm2.18  42029  jm2.19lem1  42030  jm2.22  42036  jm2.20nn  42038  proot1ex  42245  sqrtcval  42694  ofmul12  43386  binomcxplemnotnn0  43417  sineq0ALT  44000  mul13d  44288  stoweidlem11  45026  wallispi2lem1  45086  stirlinglem1  45089  stirlinglem3  45091  stirlinglem7  45095  stirlinglem15  45103  dirkertrigeqlem3  45115  dirkercncflem2  45119  fourierdlem66  45187  fourierdlem83  45204  etransclem23  45272  mod42tp1mod8  46569  fppr2odd  46698  2zlidl  46921  itcovalt2lem2lem2  47448  itsclc0yqsollem1  47536  itscnhlc0xyqsol  47539  itscnhlinecirc02plem1  47556