Theorem mul12d 11418

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  (class class class)co 7410  ℂcc 11097   · cmul 11104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-mulcom 11163  ax-mulass 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  divrec  11887  remullem  15179  sqreulem  15411  cvgrat  15937  binomrisefac  16095  tanval3  16189  sinadd  16219  dvdsmulgcd  16613  lcmgcdlem  16663  cncongr1  16724  prmdiv  16843  vdwlem6  17045  itgmulc2  25972  dvexp3  26116  aaliou3lem8  26485  dvradcnv  26560  pserdvlem2  26567  abelthlem6  26575  abelthlem7  26577  tangtx  26646  tanarg  26760  dvcxp1  26881  dvcncxp1  26884  heron  26979  dcubic1  26986  mcubic  26988  dquart  26994  quart1  26997  quartlem1  26998  asinsin  27033  lgamgulmlem2  27170  basellem3  27223  bcp1ctr  27419  gausslemma2dlem6  27512  lgseisenlem2  27516  lgseisenlem4  27518  lgsquadlem1  27520  2sqlem4  27561  chebbnd1lem3  27611  rpvmasum2  27652  mulog2sumlem3  27676  selberglem1  27685  selberg4lem1  27700  selberg3r  27709  selberg34r  27711  pntrlog2bndlem4  27720  pntrlog2bndlem6  27723  pntlemr  27742  pntlemk  27746  ostth2lem3  27775  colinearalglem4  29225  branmfn  32423  constrrtlc1  34088  constrrtcclem  34090  constrmulcl  34127  cos9thpiminplylem2  34139  vtsprod  34992  hgt750leme  35011  faclimlem1  36201  itgmulc2nc  38305  areacirclem1  38325  3factsumint2  42757  lcmineqlem10  42773  lcmineqlem11  42774  posbezout  42835  readvrec2  43090  pellexlem6  43531  pell1234qrmulcl  43552  rmxyadd  43618  jm2.18  43685  jm2.19lem1  43686  jm2.22  43692  jm2.20nn  43694  proot1ex  43893  sqrtcval  44337  ofmul12  45005  binomcxplemnotnn0  45036  sineq0ALT  45615  mul13d  45969  stoweidlem11  46695  wallispi2lem1  46755  stirlinglem1  46758  stirlinglem3  46760  stirlinglem7  46764  stirlinglem15  46772  dirkertrigeqlem3  46784  dirkercncflem2  46788  fourierdlem66  46856  fourierdlem83  46873  etransclem23  46941  cos3t  47576  sin5tlem3  47579  mod42tp1mod8  48321  nprmdvdsfacm1lem1  48339  fppr2odd  48463  2zlidl  48972  itcovalt2lem2lem2  49421  itsclc0yqsollem1  49509  itscnhlc0xyqsol  49512  itscnhlinecirc02plem1  49529