Theorem mul4d 11133

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

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcomd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcand.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		mul4d.4	. 2 ⊢ (𝜑 → 𝐷 ∈ ℂ)
5		mul4 11089	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
6	1, 2, 3, 4, 5	syl22anc 835	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7260  ℂcc 10816   · cmul 10823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-mulcl 10880  ax-mulcom 10882  ax-mulass 10884

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3071  df-v 3429  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-iota 6381  df-fv 6431  df-ov 7263

This theorem is referenced by:  remullem  14783  absmul  14950  binomrisefac  15696  cosadd  15818  tanadd  15820  eulerthlem2  16427  mul4sqlem  16598  odadd2  19394  itgmulc2  24941  plymullem1  25318  chordthmlem4  25928  heron  25931  quartlem1  25950  dchrmulcl  26340  bposlem9  26383  lgsdir  26423  lgsdi  26425  lgsquad2lem1  26475  chtppilimlem1  26564  rplogsumlem1  26575  dchrvmasumlem1  26586  dchrvmasum2lem  26587  chpdifbndlem1  26644  pntlemf  26696  brbtwn2  27216  colinearalglem4  27220  madjusmdetlem4  31722  hgt750lemf  32575  hgt750leme  32580  circum  33574  itgmulc2nc  35814  flt4lem5e  40451  pellexlem6  40614  pell1234qrmulcl  40635  rmxyadd  40701  wallispi2lem2  43545  dirkertrigeqlem3  43573  cevathlem1  44312  itsclc0xyqsolr  46045