MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul12d Structured version   Visualization version   GIF version

Theorem mul12d 10092
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
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcomd.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addcand.3 . 2 (𝜑𝐶 ∈ ℂ)
4 mul12 10049 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1317 1 (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1975  (class class class)co 6523  cc 9786   · cmul 9793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-mulcom 9852  ax-mulass 9854
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-iota 5750  df-fv 5794  df-ov 6526
This theorem is referenced by:  divrec  10546  remullem  13658  sqreulem  13889  cvgrat  14396  binomrisefac  14554  tanval3  14645  sinadd  14675  dvdsmulgcd  15054  lcmgcdlem  15099  cncongr1  15161  prmdiv  15270  vdwlem6  15470  itgmulc2  23319  dvexp3  23458  aaliou3lem8  23817  dvradcnv  23892  pserdvlem2  23899  abelthlem6  23907  abelthlem7  23909  tangtx  23974  tanarg  24082  dvcxp1  24194  dvcncxp1  24197  heron  24278  dcubic1  24285  mcubic  24287  dquart  24293  quart1  24296  quartlem1  24297  asinsin  24332  lgamgulmlem2  24469  basellem3  24522  bcp1ctr  24717  gausslemma2dlem6  24810  lgseisenlem2  24814  lgseisenlem4  24816  lgsquadlem1  24818  2sqlem4  24859  chebbnd1lem3  24873  rpvmasum2  24914  mulog2sumlem3  24938  selberglem1  24947  selberg4lem1  24962  selberg3r  24971  selberg34r  24973  pntrlog2bndlem4  24982  pntrlog2bndlem6  24985  pntlemr  25004  pntlemk  25008  ostth2lem3  25037  colinearalglem4  25503  branmfn  28150  faclimlem1  30684  itgmulc2nc  32447  areacirclem1  32469  pellexlem6  36215  pell1234qrmulcl  36236  rmxyadd  36303  jm2.18  36372  jm2.19lem1  36373  jm2.22  36379  jm2.20nn  36381  proot1ex  36597  ofmul12  37345  binomcxplemnotnn0  37376  sineq0ALT  37994  mul13d  38231  stoweidlem11  38704  wallispi2lem1  38764  stirlinglem1  38767  stirlinglem3  38769  stirlinglem7  38773  stirlinglem15  38781  dirkertrigeqlem3  38793  dirkercncflem2  38797  fourierdlem66  38865  fourierdlem83  38882  etransclem23  38950  mod42tp1mod8  39858  2zlidl  41722
  Copyright terms: Public domain W3C validator