Theorem mul12d 10565

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 10522	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1496	1 ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166  (class class class)co 6906  ℂcc 10251   · cmul 10258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-mulcom 10317  ax-mulass 10319

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-rex 3124  df-rab 3127  df-v 3417  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-iota 6087  df-fv 6132  df-ov 6909

This theorem is referenced by:  divrec  11027  remullem  14246  sqreulem  14477  cvgrat  14989  binomrisefac  15146  tanval3  15237  sinadd  15267  dvdsmulgcd  15648  lcmgcdlem  15693  cncongr1  15754  prmdiv  15862  vdwlem6  16062  itgmulc2  24000  dvexp3  24141  aaliou3lem8  24500  dvradcnv  24575  pserdvlem2  24582  abelthlem6  24590  abelthlem7  24592  tangtx  24658  tanarg  24765  dvcxp1  24884  dvcncxp1  24887  heron  24979  dcubic1  24986  mcubic  24988  dquart  24994  quart1  24997  quartlem1  24998  asinsin  25033  lgamgulmlem2  25170  basellem3  25223  bcp1ctr  25418  gausslemma2dlem6  25511  lgseisenlem2  25515  lgseisenlem4  25517  lgsquadlem1  25519  2sqlem4  25560  chebbnd1lem3  25574  rpvmasum2  25615  mulog2sumlem3  25639  selberglem1  25648  selberg4lem1  25663  selberg3r  25672  selberg34r  25674  pntrlog2bndlem4  25683  pntrlog2bndlem6  25686  pntlemr  25705  pntlemk  25709  ostth2lem3  25738  colinearalglem4  26209  branmfn  29520  vtsprod  31267  hgt750leme  31286  faclimlem1  32172  itgmulc2nc  34022  areacirclem1  34044  pellexlem6  38243  pell1234qrmulcl  38264  rmxyadd  38330  jm2.18  38399  jm2.19lem1  38400  jm2.22  38406  jm2.20nn  38408  proot1ex  38623  ofmul12  39365  binomcxplemnotnn0  39396  sineq0ALT  39992  mul13d  40291  stoweidlem11  41023  wallispi2lem1  41083  stirlinglem1  41086  stirlinglem3  41088  stirlinglem7  41092  stirlinglem15  41100  dirkertrigeqlem3  41112  dirkercncflem2  41116  fourierdlem66  41184  fourierdlem83  41201  etransclem23  41269  mod42tp1mod8  42350  2zlidl  42782  itsclc0lem2  43310  itsclc0lem5  43313