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

Theorem mul4d 10829
Description: Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
muld.1 (𝜑𝐴 ∈ ℂ)
addcomd.2 (𝜑𝐵 ∈ ℂ)
addcand.3 (𝜑𝐶 ∈ ℂ)
mul4d.4 (𝜑𝐷 ∈ ℂ)
Assertion
Ref Expression
mul4d (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))

Proof of Theorem mul4d
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcomd.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addcand.3 . 2 (𝜑𝐶 ∈ ℂ)
4 mul4d.4 . 2 (𝜑𝐷 ∈ ℂ)
5 mul4 10785 . 2 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
61, 2, 3, 4, 5syl22anc 837 1 (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  (class class class)co 7130  cc 10512   · cmul 10519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-mulcl 10576  ax-mulcom 10578  ax-mulass 10580
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-iota 6287  df-fv 6336  df-ov 7133
This theorem is referenced by:  remullem  14466  absmul  14633  binomrisefac  15375  cosadd  15497  tanadd  15499  eulerthlem2  16096  mul4sqlem  16266  odadd2  18948  itgmulc2  24416  plymullem1  24790  chordthmlem4  25400  heron  25403  quartlem1  25422  dchrmulcl  25812  bposlem9  25855  lgsdir  25895  lgsdi  25897  lgsquad2lem1  25947  chtppilimlem1  26036  rplogsumlem1  26047  dchrvmasumlem1  26058  dchrvmasum2lem  26059  chpdifbndlem1  26116  pntlemf  26168  brbtwn2  26678  colinearalglem4  26682  madjusmdetlem4  31106  hgt750lemf  31932  hgt750leme  31937  circum  32925  itgmulc2nc  35011  pellexlem6  39586  pell1234qrmulcl  39607  rmxyadd  39673  wallispi2lem2  42537  dirkertrigeqlem3  42565  cevathlem1  43304  itsclc0xyqsolr  44994
  Copyright terms: Public domain W3C validator