Theorem mul12d 11444

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127   · cmul 11134

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-mulcom 11193  ax-mulass 11195

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408

This theorem is referenced by:  divrec  11912  remullem  15147  sqreulem  15378  cvgrat  15899  binomrisefac  16058  tanval3  16152  sinadd  16182  dvdsmulgcd  16575  lcmgcdlem  16625  cncongr1  16686  prmdiv  16804  vdwlem6  17006  itgmulc2  25787  dvexp3  25934  aaliou3lem8  26305  dvradcnv  26382  pserdvlem2  26390  abelthlem6  26398  abelthlem7  26400  tangtx  26466  tanarg  26580  dvcxp1  26701  dvcncxp1  26704  heron  26800  dcubic1  26807  mcubic  26809  dquart  26815  quart1  26818  quartlem1  26819  asinsin  26854  lgamgulmlem2  26992  basellem3  27045  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  28888  branmfn  32086  constrrtlc1  33766  constrrtcclem  33768  constrmulcl  33805  cos9thpiminplylem2  33817  vtsprod  34671  hgt750leme  34690  faclimlem1  35760  itgmulc2nc  37712  areacirclem1  37732  3factsumint2  42035  lcmineqlem10  42051  lcmineqlem11  42052  posbezout  42113  readvrec2  42404  pellexlem6  42857  pell1234qrmulcl  42878  rmxyadd  42945  jm2.18  43012  jm2.19lem1  43013  jm2.22  43019  jm2.20nn  43021  proot1ex  43220  sqrtcval  43665  ofmul12  44349  binomcxplemnotnn0  44380  sineq0ALT  44961  mul13d  45308  stoweidlem11  46040  wallispi2lem1  46100  stirlinglem1  46103  stirlinglem3  46105  stirlinglem7  46109  stirlinglem15  46117  dirkertrigeqlem3  46129  dirkercncflem2  46133  fourierdlem66  46201  fourierdlem83  46218  etransclem23  46286  mod42tp1mod8  47616  fppr2odd  47745  2zlidl  48215  itcovalt2lem2lem2  48654  itsclc0yqsollem1  48742  itscnhlc0xyqsol  48745  itscnhlinecirc02plem1  48762