Theorem mul12d 11446

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7416  ℂcc 11125   · cmul 11132

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-mulcom 11191  ax-mulass 11193

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  divrec  11915  remullem  15217  sqreulem  15449  cvgrat  15974  binomrisefac  16132  tanval3  16226  sinadd  16256  dvdsmulgcd  16650  lcmgcdlem  16700  cncongr1  16761  prmdiv  16880  vdwlem6  17082  itgmulc2  26066  dvexp3  26210  aaliou3lem8  26581  dvradcnv  26657  pserdvlem2  26664  abelthlem6  26672  abelthlem7  26674  tangtx  26743  tanarg  26857  dvcxp1  26978  dvcncxp1  26981  heron  27076  dcubic1  27083  mcubic  27085  dquart  27091  quart1  27094  quartlem1  27095  asinsin  27130  lgamgulmlem2  27267  basellem3  27320  bcp1ctr  27516  gausslemma2dlem6  27609  lgseisenlem2  27613  lgseisenlem4  27615  lgsquadlem1  27617  2sqlem4  27658  chebbnd1lem3  27708  rpvmasum2  27749  mulog2sumlem3  27773  selberglem1  27782  selberg4lem1  27797  selberg3r  27806  selberg34r  27808  pntrlog2bndlem4  27817  pntrlog2bndlem6  27820  pntlemr  27839  pntlemk  27843  ostth2lem3  27872  colinearalglem4  29367  branmfn  32587  constrrtlc1  34244  constrrtcclem  34246  constrmulcl  34283  cos9thpiminplylem2  34295  vtsprod  35149  hgt750leme  35168  faclimlem1  36324  itgmulc2nc  38439  areacirclem1  38459  3factsumint2  42890  lcmineqlem10  42906  lcmineqlem11  42907  posbezout  42968  readvrec2  43238  pellexlem6  43677  pell1234qrmulcl  43698  rmxyadd  43764  jm2.18  43831  jm2.19lem1  43832  jm2.22  43838  jm2.20nn  43840  proot1ex  44039  sqrtcval  44483  ofmul12  45151  binomcxplemnotnn0  45182  sineq0ALT  45761  mul13d  46115  stoweidlem11  46841  wallispi2lem1  46901  stirlinglem1  46904  stirlinglem3  46906  stirlinglem7  46910  stirlinglem15  46918  dirkertrigeqlem3  46930  dirkercncflem2  46934  fourierdlem66  47002  fourierdlem83  47019  etransclem23  47087  cos3t  47738  sin5tlem3  47741  mod42tp1mod8  48507  nprmdvdsfacm1lem1  48525  fppr2odd  48649  2zlidl  49157  itcovalt2lem2lem2  49606  itsclc0yqsollem1  49694  itscnhlc0xyqsol  49697  itscnhlinecirc02plem1  49714