Theorem mul12d 11520

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11199   · cmul 11206

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-mulcom 11265  ax-mulass 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  divrec  11991  remullem  15296  sqreulem  15528  cvgrat  16053  binomrisefac  16209  tanval3  16303  sinadd  16333  dvdsmulgcd  16731  lcmgcdlem  16782  cncongr1  16843  prmdiv  16963  vdwlem6  17165  itgmulc2  26155  dvexp3  26299  aaliou3lem8  26673  dvradcnv  26749  pserdvlem2  26756  abelthlem6  26764  abelthlem7  26766  tangtx  26835  tanarg  26948  dvcxp1  27069  dvcncxp1  27072  heron  27167  dcubic1  27174  mcubic  27176  dquart  27182  quart1  27185  quartlem1  27186  asinsin  27221  lgamgulmlem2  27358  basellem3  27411  bcp1ctr  27607  gausslemma2dlem6  27700  lgseisenlem2  27704  lgseisenlem4  27706  lgsquadlem1  27708  2sqlem4  27749  chebbnd1lem3  27799  rpvmasum2  27840  mulog2sumlem3  27864  selberglem1  27873  selberg4lem1  27888  selberg3r  27897  selberg34r  27899  pntrlog2bndlem4  27908  pntrlog2bndlem6  27911  pntlemr  27930  pntlemk  27934  ostth2lem3  27963  colinearalglem4  29488  branmfn  32708  constrrtlc1  34407  constrrtcclem  34409  constrmulcl  34446  cos9thpiminplylem2  34458  vtsprod  35311  hgt750leme  35330  faclimlem1  36583  itgmulc2nc  38682  areacirclem1  38702  3factsumint2  43148  lcmineqlem10  43164  lcmineqlem11  43165  posbezout  43226  readvrec2  43488  pellexlem6  43917  pell1234qrmulcl  43938  rmxyadd  44004  jm2.18  44071  jm2.19lem1  44072  jm2.22  44078  jm2.20nn  44080  proot1ex  44274  sqrtcval  44717  ofmul12  45385  binomcxplemnotnn0  45416  sineq0ALT  45995  mul13d  46372  stoweidlem11  47097  wallispi2lem1  47157  stirlinglem1  47160  stirlinglem3  47162  stirlinglem7  47166  stirlinglem15  47174  dirkertrigeqlem3  47186  dirkercncflem2  47190  fourierdlem66  47258  fourierdlem83  47275  etransclem23  47343  cos3t  47994  sin5tlem3  47997  mod42tp1mod8  48763  nprmdvdsfacm1lem1  48781  fppr2odd  48905  2zlidl  49413  itcovalt2lem2lem2  49862  itsclc0yqsollem1  49950  itscnhlc0xyqsol  49953  itscnhlinecirc02plem1  49970