Theorem mul12d 11468

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151   · cmul 11158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-mulcom 11217  ax-mulass 11219

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434

This theorem is referenced by:  divrec  11936  remullem  15164  sqreulem  15395  cvgrat  15916  binomrisefac  16075  tanval3  16167  sinadd  16197  dvdsmulgcd  16590  lcmgcdlem  16640  cncongr1  16701  prmdiv  16819  vdwlem6  17020  itgmulc2  25884  dvexp3  26031  aaliou3lem8  26402  dvradcnv  26479  pserdvlem2  26487  abelthlem6  26495  abelthlem7  26497  tangtx  26562  tanarg  26676  dvcxp1  26797  dvcncxp1  26800  heron  26896  dcubic1  26903  mcubic  26905  dquart  26911  quart1  26914  quartlem1  26915  asinsin  26950  lgamgulmlem2  27088  basellem3  27141  bcp1ctr  27338  gausslemma2dlem6  27431  lgseisenlem2  27435  lgseisenlem4  27437  lgsquadlem1  27439  2sqlem4  27480  chebbnd1lem3  27530  rpvmasum2  27571  mulog2sumlem3  27595  selberglem1  27604  selberg4lem1  27619  selberg3r  27628  selberg34r  27630  pntrlog2bndlem4  27639  pntrlog2bndlem6  27642  pntlemr  27661  pntlemk  27665  ostth2lem3  27694  colinearalglem4  28939  branmfn  32134  constrrtlc1  33738  constrrtcclem  33740  vtsprod  34633  hgt750leme  34652  faclimlem1  35723  itgmulc2nc  37675  areacirclem1  37695  3factsumint2  42004  lcmineqlem10  42020  lcmineqlem11  42021  posbezout  42082  readvrec2  42370  pellexlem6  42822  pell1234qrmulcl  42843  rmxyadd  42910  jm2.18  42977  jm2.19lem1  42978  jm2.22  42984  jm2.20nn  42986  proot1ex  43185  sqrtcval  43631  ofmul12  44321  binomcxplemnotnn0  44352  sineq0ALT  44935  mul13d  45230  stoweidlem11  45967  wallispi2lem1  46027  stirlinglem1  46030  stirlinglem3  46032  stirlinglem7  46036  stirlinglem15  46044  dirkertrigeqlem3  46056  dirkercncflem2  46060  fourierdlem66  46128  fourierdlem83  46145  etransclem23  46213  mod42tp1mod8  47527  fppr2odd  47656  2zlidl  48084  itcovalt2lem2lem2  48524  itsclc0yqsollem1  48612  itscnhlc0xyqsol  48615  itscnhlinecirc02plem1  48632