Theorem mul12d 11499

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-mulcom 11248  ax-mulass 11250

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  divrec  11965  remullem  15177  sqreulem  15408  cvgrat  15931  binomrisefac  16090  tanval3  16182  sinadd  16212  dvdsmulgcd  16603  lcmgcdlem  16653  cncongr1  16714  prmdiv  16832  vdwlem6  17033  itgmulc2  25889  dvexp3  26036  aaliou3lem8  26405  dvradcnv  26482  pserdvlem2  26490  abelthlem6  26498  abelthlem7  26500  tangtx  26565  tanarg  26679  dvcxp1  26800  dvcncxp1  26803  heron  26899  dcubic1  26906  mcubic  26908  dquart  26914  quart1  26917  quartlem1  26918  asinsin  26953  lgamgulmlem2  27091  basellem3  27144  bcp1ctr  27341  gausslemma2dlem6  27434  lgseisenlem2  27438  lgseisenlem4  27440  lgsquadlem1  27442  2sqlem4  27483  chebbnd1lem3  27533  rpvmasum2  27574  mulog2sumlem3  27598  selberglem1  27607  selberg4lem1  27622  selberg3r  27631  selberg34r  27633  pntrlog2bndlem4  27642  pntrlog2bndlem6  27645  pntlemr  27664  pntlemk  27668  ostth2lem3  27697  colinearalglem4  28942  branmfn  32137  constrrtlc1  33723  constrrtcclem  33725  vtsprod  34616  hgt750leme  34635  faclimlem1  35705  itgmulc2nc  37648  areacirclem1  37668  3factsumint2  41979  lcmineqlem10  41995  lcmineqlem11  41996  posbezout  42057  pellexlem6  42790  pell1234qrmulcl  42811  rmxyadd  42878  jm2.18  42945  jm2.19lem1  42946  jm2.22  42952  jm2.20nn  42954  proot1ex  43157  sqrtcval  43603  ofmul12  44294  binomcxplemnotnn0  44325  sineq0ALT  44908  mul13d  45194  stoweidlem11  45932  wallispi2lem1  45992  stirlinglem1  45995  stirlinglem3  45997  stirlinglem7  46001  stirlinglem15  46009  dirkertrigeqlem3  46021  dirkercncflem2  46025  fourierdlem66  46093  fourierdlem83  46110  etransclem23  46178  mod42tp1mod8  47476  fppr2odd  47605  2zlidl  47963  itcovalt2lem2lem2  48408  itsclc0yqsollem1  48496  itscnhlc0xyqsol  48499  itscnhlinecirc02plem1  48516