Theorem mul12d 11378

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  (class class class)co 7381  ℂcc 11057   · cmul 11064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-mulcom 11123  ax-mulass 11125

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384

This theorem is referenced by:  divrec  11847  remullem  15127  sqreulem  15359  cvgrat  15885  binomrisefac  16044  tanval3  16138  sinadd  16168  dvdsmulgcd  16562  lcmgcdlem  16612  cncongr1  16673  prmdiv  16792  vdwlem6  16994  itgmulc2  25865  dvexp3  26009  aaliou3lem8  26375  dvradcnv  26450  pserdvlem2  26457  abelthlem6  26465  abelthlem7  26467  tangtx  26536  tanarg  26650  dvcxp1  26771  dvcncxp1  26774  heron  26869  dcubic1  26876  mcubic  26878  dquart  26884  quart1  26887  quartlem1  26888  asinsin  26923  lgamgulmlem2  27060  basellem3  27113  bcp1ctr  27309  gausslemma2dlem6  27402  lgseisenlem2  27406  lgseisenlem4  27408  lgsquadlem1  27410  2sqlem4  27451  chebbnd1lem3  27501  rpvmasum2  27542  mulog2sumlem3  27566  selberglem1  27575  selberg4lem1  27590  selberg3r  27599  selberg34r  27601  pntrlog2bndlem4  27610  pntrlog2bndlem6  27613  pntlemr  27632  pntlemk  27636  ostth2lem3  27665  colinearalglem4  29045  branmfn  32243  constrrtlc1  33973  constrrtcclem  33975  constrmulcl  34012  cos9thpiminplylem2  34024  vtsprod  34880  hgt750leme  34899  faclimlem1  36031  itgmulc2nc  38125  areacirclem1  38145  3factsumint2  42577  lcmineqlem10  42593  lcmineqlem11  42594  posbezout  42655  readvrec2  42908  pellexlem6  43349  pell1234qrmulcl  43370  rmxyadd  43436  jm2.18  43503  jm2.19lem1  43504  jm2.22  43510  jm2.20nn  43512  proot1ex  43711  sqrtcval  44155  ofmul12  44839  binomcxplemnotnn0  44870  sineq0ALT  45450  mul13d  45797  stoweidlem11  46523  wallispi2lem1  46583  stirlinglem1  46586  stirlinglem3  46588  stirlinglem7  46592  stirlinglem15  46600  dirkertrigeqlem3  46612  dirkercncflem2  46616  fourierdlem66  46684  fourierdlem83  46701  etransclem23  46769  cos3t  47404  sin5tlem3  47407  mod42tp1mod8  48149  nprmdvdsfacm1lem1  48167  fppr2odd  48291  2zlidl  48800  itcovalt2lem2lem2  49234  itsclc0yqsollem1  49322  itscnhlc0xyqsol  49325  itscnhlinecirc02plem1  49342