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

Theorem mul4d 10454
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 10411 . 2 (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
61, 2, 3, 4, 5syl22anc 1477 1 (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145  (class class class)co 6796  cc 10140   · cmul 10147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-mulcl 10204  ax-mulcom 10206  ax-mulass 10208
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5993  df-fv 6038  df-ov 6799
This theorem is referenced by:  remullem  14076  absmul  14242  binomrisefac  14979  cosadd  15101  tanadd  15103  eulerthlem2  15694  mul4sqlem  15864  odadd2  18459  itgmulc2  23820  plymullem1  24190  chordthmlem4  24783  heron  24786  quartlem1  24805  dchrmulcl  25195  bposlem9  25238  lgsdir  25278  lgsdi  25280  lgsquad2lem1  25330  chtppilimlem1  25383  rplogsumlem1  25394  dchrvmasumlem1  25405  dchrvmasum2lem  25406  chpdifbndlem1  25463  pntlemf  25515  brbtwn2  26006  colinearalglem4  26010  madjusmdetlem4  30236  hgt750lemf  31071  hgt750leme  31076  circum  31906  itgmulc2nc  33810  pellexlem6  37924  pell1234qrmulcl  37945  rmxyadd  38012  wallispi2lem2  40803  dirkertrigeqlem3  40831  cevathlem1  41573
  Copyright terms: Public domain W3C validator