Theorem mul12d 11355

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   · cmul 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-mulcom 11102  ax-mulass 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6455  df-fv 6507  df-ov 7370

This theorem is referenced by:  divrec  11825  remullem  15090  sqreulem  15322  cvgrat  15848  binomrisefac  16007  tanval3  16101  sinadd  16131  dvdsmulgcd  16525  lcmgcdlem  16575  cncongr1  16636  prmdiv  16755  vdwlem6  16957  itgmulc2  25801  dvexp3  25945  aaliou3lem8  26311  dvradcnv  26386  pserdvlem2  26393  abelthlem6  26401  abelthlem7  26403  tangtx  26469  tanarg  26583  dvcxp1  26704  dvcncxp1  26707  heron  26802  dcubic1  26809  mcubic  26811  dquart  26817  quart1  26820  quartlem1  26821  asinsin  26856  lgamgulmlem2  26993  basellem3  27046  bcp1ctr  27242  gausslemma2dlem6  27335  lgseisenlem2  27339  lgseisenlem4  27341  lgsquadlem1  27343  2sqlem4  27384  chebbnd1lem3  27434  rpvmasum2  27475  mulog2sumlem3  27499  selberglem1  27508  selberg4lem1  27523  selberg3r  27532  selberg34r  27534  pntrlog2bndlem4  27543  pntrlog2bndlem6  27546  pntlemr  27565  pntlemk  27569  ostth2lem3  27598  colinearalglem4  28978  branmfn  32176  constrrtlc1  33876  constrrtcclem  33878  constrmulcl  33915  cos9thpiminplylem2  33927  vtsprod  34783  hgt750leme  34802  faclimlem1  35925  itgmulc2nc  38009  areacirclem1  38029  3factsumint2  42461  lcmineqlem10  42477  lcmineqlem11  42478  posbezout  42539  readvrec2  42793  pellexlem6  43262  pell1234qrmulcl  43283  rmxyadd  43349  jm2.18  43416  jm2.19lem1  43417  jm2.22  43423  jm2.20nn  43425  proot1ex  43624  sqrtcval  44068  ofmul12  44752  binomcxplemnotnn0  44783  sineq0ALT  45363  mul13d  45713  stoweidlem11  46439  wallispi2lem1  46499  stirlinglem1  46502  stirlinglem3  46504  stirlinglem7  46508  stirlinglem15  46516  dirkertrigeqlem3  46528  dirkercncflem2  46532  fourierdlem66  46600  fourierdlem83  46617  etransclem23  46685  cos3t  47318  sin5tlem3  47321  mod42tp1mod8  48059  nprmdvdsfacm1lem1  48077  fppr2odd  48201  2zlidl  48710  itcovalt2lem2lem2  49144  itsclc0yqsollem1  49232  itscnhlc0xyqsol  49235  itscnhlinecirc02plem1  49252