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

Theorem mul32d 10838
Description: Commutative/associative law that swaps the last 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
mul32d (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))

Proof of Theorem mul32d
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcomd.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addcand.3 . 2 (𝜑𝐶 ∈ ℂ)
4 mul32 10794 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
51, 2, 3, 4syl3anc 1363 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-mulcom 10589  ax-mulass 10591
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  conjmul  11345  modmul1  13280  binom3  13573  bernneq  13578  expmulnbnd  13584  discr  13589  bcm1k  13663  bcp1n  13664  reccn2  14941  binomlem  15172  binomfallfaclem2  15382  tanadd  15508  eirrlem  15545  dvds2ln  15630  bezoutlem4  15878  divgcdcoprm0  15997  modprm0  16130  nrginvrcnlem  23227  tcphcphlem2  23766  csbren  23929  radcnvlem1  24928  tanarg  25129  cxpeq  25265  quad2  25344  binom4  25355  dquartlem2  25357  dquart  25358  quart1lem  25360  dvatan  25440  log2cnv  25449  basellem8  25592  bcmono  25780  gausslemma2d  25877  lgsquadlem1  25883  2lgslem3b  25900  2lgslem3c  25901  2lgslem3d  25902  rplogsumlem1  25987  dchrisumlem2  25993  chpdifbndlem1  26056  selberg3lem1  26060  selberg4  26064  selberg3r  26072  pntrlog2bndlem2  26081  pntrlog2bndlem3  26082  pntrlog2bndlem5  26084  pntlemf  26108  pntlemo  26110  ostth2lem1  26121  ostth2lem3  26138  logdivsqrle  31820  circum  32814  jm2.25  39474  jm2.27c  39482  binomcxplemnotnn0  40565  dvasinbx  42081  stirlinglem3  42238  dirkercncflem2  42266  cevathlem1  43001  itschlc0yqe  44675
  Copyright terms: Public domain W3C validator