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

Theorem mul32d 10447
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 10404 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
51, 2, 3, 4syl3anc 1475 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  wcel 2144  (class class class)co 6792  cc 10135   · cmul 10142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-mulcom 10201  ax-mulass 10203
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-iota 5994  df-fv 6039  df-ov 6795
This theorem is referenced by:  conjmul  10943  modmul1  12930  binom3  13191  bernneq  13196  expmulnbnd  13202  discr  13207  bcm1k  13305  bcp1n  13306  reccn2  14534  binomlem  14767  binomfallfaclem2  14976  tanadd  15102  eirrlem  15137  dvds2ln  15222  bezoutlem4  15466  divgcdcoprm0  15585  modprm0  15716  nrginvrcnlem  22714  tchcphlem2  23253  csbren  23400  radcnvlem1  24386  tanarg  24585  cxpeq  24718  quad2  24786  binom4  24797  dquartlem2  24799  dquart  24800  quart1lem  24802  dvatan  24882  log2cnv  24891  basellem8  25034  bcmono  25222  gausslemma2d  25319  lgsquadlem1  25325  2lgslem3b  25342  2lgslem3c  25343  2lgslem3d  25344  rplogsumlem1  25393  dchrisumlem2  25399  chpdifbndlem1  25462  selberg3lem1  25466  selberg4  25470  selberg3r  25478  pntrlog2bndlem2  25487  pntrlog2bndlem3  25488  pntrlog2bndlem5  25490  pntlemf  25514  pntlemo  25516  ostth2lem1  25527  ostth2lem3  25544  logdivsqrle  31062  circum  31900  jm2.25  38085  jm2.27c  38093  binomcxplemnotnn0  39074  dvasinbx  40647  stirlinglem3  40804  dirkercncflem2  40832  cevathlem1  41570
  Copyright terms: Public domain W3C validator