Theorem mul4d 11328

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 11284	. 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
6	1, 2, 3, 4, 5	syl22anc 838	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   · cmul 11014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-mulcl 11071  ax-mulcom 11073  ax-mulass 11075

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  remullem  15035  absmul  15201  binomrisefac  15949  cosadd  16074  tanadd  16076  eulerthlem2  16693  mul4sqlem  16865  odadd2  19728  itgmulc2  25733  plymullem1  26117  chordthmlem4  26743  heron  26746  quartlem1  26765  dchrmulcl  27158  bposlem9  27201  lgsdir  27241  lgsdi  27243  lgsquad2lem1  27293  chtppilimlem1  27382  rplogsumlem1  27393  dchrvmasumlem1  27404  dchrvmasum2lem  27405  chpdifbndlem1  27462  pntlemf  27514  brbtwn2  28850  colinearalglem4  28854  binom2subadd  32685  zringfrac  33491  constrmulcl  33738  madjusmdetlem4  33797  hgt750lemf  34621  hgt750leme  34626  circum  35651  itgmulc2nc  37672  flt4lem5e  42633  pellexlem6  42811  pell1234qrmulcl  42832  rmxyadd  42898  wallispi2lem2  46057  dirkertrigeqlem3  46085  cevathlem1  46852  itsclc0xyqsolr  48758