Theorem mul12d 11390

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   · cmul 11080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-mulcom 11139  ax-mulass 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  divrec  11860  remullem  15101  sqreulem  15333  cvgrat  15856  binomrisefac  16015  tanval3  16109  sinadd  16139  dvdsmulgcd  16533  lcmgcdlem  16583  cncongr1  16644  prmdiv  16762  vdwlem6  16964  itgmulc2  25742  dvexp3  25889  aaliou3lem8  26260  dvradcnv  26337  pserdvlem2  26345  abelthlem6  26353  abelthlem7  26355  tangtx  26421  tanarg  26535  dvcxp1  26656  dvcncxp1  26659  heron  26755  dcubic1  26762  mcubic  26764  dquart  26770  quart1  26773  quartlem1  26774  asinsin  26809  lgamgulmlem2  26947  basellem3  27000  bcp1ctr  27197  gausslemma2dlem6  27290  lgseisenlem2  27294  lgseisenlem4  27296  lgsquadlem1  27298  2sqlem4  27339  chebbnd1lem3  27389  rpvmasum2  27430  mulog2sumlem3  27454  selberglem1  27463  selberg4lem1  27478  selberg3r  27487  selberg34r  27489  pntrlog2bndlem4  27498  pntrlog2bndlem6  27501  pntlemr  27520  pntlemk  27524  ostth2lem3  27553  colinearalglem4  28843  branmfn  32041  constrrtlc1  33729  constrrtcclem  33731  constrmulcl  33768  cos9thpiminplylem2  33780  vtsprod  34637  hgt750leme  34656  faclimlem1  35737  itgmulc2nc  37689  areacirclem1  37709  3factsumint2  42017  lcmineqlem10  42033  lcmineqlem11  42034  posbezout  42095  readvrec2  42356  pellexlem6  42829  pell1234qrmulcl  42850  rmxyadd  42917  jm2.18  42984  jm2.19lem1  42985  jm2.22  42991  jm2.20nn  42993  proot1ex  43192  sqrtcval  43637  ofmul12  44321  binomcxplemnotnn0  44352  sineq0ALT  44933  mul13d  45285  stoweidlem11  46016  wallispi2lem1  46076  stirlinglem1  46079  stirlinglem3  46081  stirlinglem7  46085  stirlinglem15  46093  dirkertrigeqlem3  46105  dirkercncflem2  46109  fourierdlem66  46177  fourierdlem83  46194  etransclem23  46262  mod42tp1mod8  47607  fppr2odd  47736  2zlidl  48232  itcovalt2lem2lem2  48667  itsclc0yqsollem1  48755  itscnhlc0xyqsol  48758  itscnhlinecirc02plem1  48775