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

Theorem mul12d 10230
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 10187 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1324 1 (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  (class class class)co 6635  cc 9919   · cmul 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-mulcom 9985  ax-mulass 9987
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638
This theorem is referenced by:  divrec  10686  remullem  13849  sqreulem  14080  cvgrat  14596  binomrisefac  14754  tanval3  14845  sinadd  14875  dvdsmulgcd  15255  lcmgcdlem  15300  cncongr1  15362  prmdiv  15471  vdwlem6  15671  itgmulc2  23581  dvexp3  23722  aaliou3lem8  24081  dvradcnv  24156  pserdvlem2  24163  abelthlem6  24171  abelthlem7  24173  tangtx  24238  tanarg  24346  dvcxp1  24462  dvcncxp1  24465  heron  24546  dcubic1  24553  mcubic  24555  dquart  24561  quart1  24564  quartlem1  24565  asinsin  24600  lgamgulmlem2  24737  basellem3  24790  bcp1ctr  24985  gausslemma2dlem6  25078  lgseisenlem2  25082  lgseisenlem4  25084  lgsquadlem1  25086  2sqlem4  25127  chebbnd1lem3  25141  rpvmasum2  25182  mulog2sumlem3  25206  selberglem1  25215  selberg4lem1  25230  selberg3r  25239  selberg34r  25241  pntrlog2bndlem4  25250  pntrlog2bndlem6  25253  pntlemr  25272  pntlemk  25276  ostth2lem3  25305  colinearalglem4  25770  branmfn  28934  vtsprod  30691  hgt750leme  30710  faclimlem1  31604  itgmulc2nc  33449  areacirclem1  33471  pellexlem6  37217  pell1234qrmulcl  37238  rmxyadd  37305  jm2.18  37374  jm2.19lem1  37375  jm2.22  37381  jm2.20nn  37383  proot1ex  37598  ofmul12  38344  binomcxplemnotnn0  38375  sineq0ALT  38993  mul13d  39304  stoweidlem11  39991  wallispi2lem1  40051  stirlinglem1  40054  stirlinglem3  40056  stirlinglem7  40060  stirlinglem15  40068  dirkertrigeqlem3  40080  dirkercncflem2  40084  fourierdlem66  40152  fourierdlem83  40169  etransclem23  40237  mod42tp1mod8  41284  2zlidl  41699
  Copyright terms: Public domain W3C validator