Theorem mul12d 11407

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-mulcom 11152  ax-mulass 11154

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403

This theorem is referenced by:  divrec  11876  remullem  15169  sqreulem  15401  cvgrat  15927  binomrisefac  16086  tanval3  16180  sinadd  16210  dvdsmulgcd  16604  lcmgcdlem  16654  cncongr1  16715  prmdiv  16834  vdwlem6  17036  itgmulc2  25954  dvexp3  26098  aaliou3lem8  26467  dvradcnv  26542  pserdvlem2  26549  abelthlem6  26557  abelthlem7  26559  tangtx  26628  tanarg  26742  dvcxp1  26863  dvcncxp1  26866  heron  26961  dcubic1  26968  mcubic  26970  dquart  26976  quart1  26979  quartlem1  26980  asinsin  27015  lgamgulmlem2  27152  basellem3  27205  bcp1ctr  27401  gausslemma2dlem6  27494  lgseisenlem2  27498  lgseisenlem4  27500  lgsquadlem1  27502  2sqlem4  27543  chebbnd1lem3  27593  rpvmasum2  27634  mulog2sumlem3  27658  selberglem1  27667  selberg4lem1  27682  selberg3r  27691  selberg34r  27693  pntrlog2bndlem4  27702  pntrlog2bndlem6  27705  pntlemr  27724  pntlemk  27728  ostth2lem3  27757  colinearalglem4  29168  branmfn  32366  constrrtlc1  34039  constrrtcclem  34041  constrmulcl  34078  cos9thpiminplylem2  34090  vtsprod  34943  hgt750leme  34962  faclimlem1  36106  itgmulc2nc  38199  areacirclem1  38219  3factsumint2  42651  lcmineqlem10  42667  lcmineqlem11  42668  posbezout  42729  readvrec2  42982  pellexlem6  43423  pell1234qrmulcl  43444  rmxyadd  43510  jm2.18  43577  jm2.19lem1  43578  jm2.22  43584  jm2.20nn  43586  proot1ex  43785  sqrtcval  44229  ofmul12  44899  binomcxplemnotnn0  44930  sineq0ALT  45510  mul13d  45857  stoweidlem11  46583  wallispi2lem1  46643  stirlinglem1  46646  stirlinglem3  46648  stirlinglem7  46652  stirlinglem15  46660  dirkertrigeqlem3  46672  dirkercncflem2  46676  fourierdlem66  46744  fourierdlem83  46761  etransclem23  46829  cos3t  47464  sin5tlem3  47467  mod42tp1mod8  48209  nprmdvdsfacm1lem1  48227  fppr2odd  48351  2zlidl  48860  itcovalt2lem2lem2  49305  itsclc0yqsollem1  49393  itscnhlc0xyqsol  49396  itscnhlinecirc02plem1  49413