Theorem mul4d 11233

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7307  ℂcc 10915   · cmul 10922

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-mulcl 10979  ax-mulcom 10981  ax-mulass 10983

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310

This theorem is referenced by:  remullem  14884  absmul  15051  binomrisefac  15797  cosadd  15919  tanadd  15921  eulerthlem2  16528  mul4sqlem  16699  odadd2  19495  itgmulc2  25043  plymullem1  25420  chordthmlem4  26030  heron  26033  quartlem1  26052  dchrmulcl  26442  bposlem9  26485  lgsdir  26525  lgsdi  26527  lgsquad2lem1  26577  chtppilimlem1  26666  rplogsumlem1  26677  dchrvmasumlem1  26688  dchrvmasum2lem  26689  chpdifbndlem1  26746  pntlemf  26798  brbtwn2  27318  colinearalglem4  27322  madjusmdetlem4  31825  hgt750lemf  32678  hgt750leme  32683  circum  33677  itgmulc2nc  35889  flt4lem5e  40530  pellexlem6  40693  pell1234qrmulcl  40714  rmxyadd  40781  wallispi2lem2  43662  dirkertrigeqlem3  43690  cevathlem1  44441  itsclc0xyqsolr  46173