Theorem mul4d 11452

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   · cmul 11139

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 2708  ax-mulcl 11196  ax-mulcom 11198  ax-mulass 11200

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413

This theorem is referenced by:  remullem  15152  absmul  15318  binomrisefac  16063  cosadd  16188  tanadd  16190  eulerthlem2  16806  mul4sqlem  16978  odadd2  19835  itgmulc2  25792  plymullem1  26176  chordthmlem4  26802  heron  26805  quartlem1  26824  dchrmulcl  27217  bposlem9  27260  lgsdir  27300  lgsdi  27302  lgsquad2lem1  27352  chtppilimlem1  27441  rplogsumlem1  27452  dchrvmasumlem1  27463  dchrvmasum2lem  27464  chpdifbndlem1  27521  pntlemf  27573  brbtwn2  28889  colinearalglem4  28893  binom2subadd  32724  zringfrac  33574  constrmulcl  33810  madjusmdetlem4  33866  hgt750lemf  34690  hgt750leme  34695  circum  35701  itgmulc2nc  37717  flt4lem5e  42646  pellexlem6  42824  pell1234qrmulcl  42845  rmxyadd  42912  wallispi2lem2  46068  dirkertrigeqlem3  46096  cevathlem1  46863  itsclc0xyqsolr  48716