Theorem mul12d 10892

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7155  ℂcc 10578   · cmul 10585

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-mulcom 10644  ax-mulass 10646

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-iota 6298  df-fv 6347  df-ov 7158

This theorem is referenced by:  divrec  11357  remullem  14540  sqreulem  14772  cvgrat  15292  binomrisefac  15449  tanval3  15540  sinadd  15570  dvdsmulgcd  15961  lcmgcdlem  16007  cncongr1  16068  prmdiv  16182  vdwlem6  16382  itgmulc2  24538  dvexp3  24682  aaliou3lem8  25045  dvradcnv  25120  pserdvlem2  25127  abelthlem6  25135  abelthlem7  25137  tangtx  25202  tanarg  25314  dvcxp1  25433  dvcncxp1  25436  heron  25528  dcubic1  25535  mcubic  25537  dquart  25543  quart1  25546  quartlem1  25547  asinsin  25582  lgamgulmlem2  25719  basellem3  25772  bcp1ctr  25967  gausslemma2dlem6  26060  lgseisenlem2  26064  lgseisenlem4  26066  lgsquadlem1  26068  2sqlem4  26109  chebbnd1lem3  26159  rpvmasum2  26200  mulog2sumlem3  26224  selberglem1  26233  selberg4lem1  26248  selberg3r  26257  selberg34r  26259  pntrlog2bndlem4  26268  pntrlog2bndlem6  26271  pntlemr  26290  pntlemk  26294  ostth2lem3  26323  colinearalglem4  26807  branmfn  29992  vtsprod  32142  hgt750leme  32161  faclimlem1  33228  itgmulc2nc  35431  areacirclem1  35451  3factsumint2  39615  lcmineqlem10  39631  lcmineqlem11  39632  pellexlem6  40176  pell1234qrmulcl  40197  rmxyadd  40263  jm2.18  40330  jm2.19lem1  40331  jm2.22  40337  jm2.20nn  40339  proot1ex  40546  sqrtcval  40742  ofmul12  41430  binomcxplemnotnn0  41461  sineq0ALT  42044  mul13d  42306  stoweidlem11  43047  wallispi2lem1  43107  stirlinglem1  43110  stirlinglem3  43112  stirlinglem7  43116  stirlinglem15  43124  dirkertrigeqlem3  43136  dirkercncflem2  43140  fourierdlem66  43208  fourierdlem83  43225  etransclem23  43293  mod42tp1mod8  44515  fppr2odd  44644  2zlidl  44953  itcovalt2lem2lem2  45481  itsclc0yqsollem1  45569  itscnhlc0xyqsol  45572  itscnhlinecirc02plem1  45589