Theorem mul12d 11546

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   · cmul 11232

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-mulcom 11291  ax-mulass 11293

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446

This theorem is used by:  divrec  12017  remullem  15324  sqreulem  15556  cvgrat  16081  binomrisefac  16237  tanval3  16331  sinadd  16361  dvdsmulgcd  16759  lcmgcdlem  16810  cncongr1  16871  prmdiv  16991  vdwlem6  17193  itgmulc2  26184  dvexp3  26328  aaliou3lem8  26702  dvradcnv  26778  pserdvlem2  26785  abelthlem6  26793  abelthlem7  26795  tangtx  26864  tanarg  26977  dvcxp1  27098  dvcncxp1  27101  heron  27196  dcubic1  27203  mcubic  27205  dquart  27211  quart1  27214  quartlem1  27215  asinsin  27250  lgamgulmlem2  27387  basellem3  27440  bcp1ctr  27636  gausslemma2dlem6  27729  lgseisenlem2  27733  lgseisenlem4  27735  lgsquadlem1  27737  2sqlem4  27778  chebbnd1lem3  27828  rpvmasum2  27869  mulog2sumlem3  27893  selberglem1  27902  selberg4lem1  27917  selberg3r  27926  selberg34r  27928  pntrlog2bndlem4  27937  pntrlog2bndlem6  27940  pntlemr  27959  pntlemk  27963  ostth2lem3  27992  colinearalglem4  29517  branmfn  32737  constrrtlc1  34434  constrrtcclem  34436  constrmulcl  34473  cos9thpiminplylem2  34485  vtsprod  35338  hgt750leme  35357  faclimlem1  36686  itgmulc2nc  38798  areacirclem1  38818  3factsumint2  43264  lcmineqlem10  43280  lcmineqlem11  43281  posbezout  43342  readvrec2  43605  pellexlem6  44034  pell1234qrmulcl  44055  rmxyadd  44121  jm2.18  44188  jm2.19lem1  44189  jm2.22  44195  jm2.20nn  44197  proot1ex  44390  sqrtcval  44833  ofmul12  45501  binomcxplemnotnn0  45532  sineq0ALT  46110  mul13d  46501  stoweidlem11  47226  wallispi2lem1  47286  stirlinglem1  47289  stirlinglem3  47291  stirlinglem7  47295  stirlinglem15  47303  dirkertrigeqlem3  47315  dirkercncflem2  47319  fourierdlem66  47387  fourierdlem83  47404  etransclem23  47472  cos3t  48123  sin5tlem3  48126  mod42tp1mod8  48892  nprmdvdsfacm1lem1  48910  fppr2odd  49034  2zlidl  49542  itcovalt2lem2lem2  49991  itsclc0yqsollem1  50079  itscnhlc0xyqsol  50082  itscnhlinecirc02plem1  50099