![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mul4d | Structured version Visualization version GIF version |
Description: Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
muld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcomd.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
addcand.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
mul4d.4 | ⊢ (𝜑 → 𝐷 ∈ ℂ) |
Ref | Expression |
---|---|
mul4d | ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcomd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | addcand.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | mul4d.4 | . 2 ⊢ (𝜑 → 𝐷 ∈ ℂ) | |
5 | mul4 10544 | . 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) | |
6 | 1, 2, 3, 4, 5 | syl22anc 829 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 (class class class)co 6922 ℂcc 10270 · cmul 10277 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-mulcl 10334 ax-mulcom 10336 ax-mulass 10338 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-iota 6099 df-fv 6143 df-ov 6925 |
This theorem is referenced by: remullem 14275 absmul 14441 binomrisefac 15175 cosadd 15297 tanadd 15299 eulerthlem2 15891 mul4sqlem 16061 odadd2 18638 itgmulc2 24037 plymullem1 24407 chordthmlem4 25013 heron 25016 quartlem1 25035 dchrmulcl 25426 bposlem9 25469 lgsdir 25509 lgsdi 25511 lgsquad2lem1 25561 chtppilimlem1 25614 rplogsumlem1 25625 dchrvmasumlem1 25636 dchrvmasum2lem 25637 chpdifbndlem1 25694 pntlemf 25746 brbtwn2 26254 colinearalglem4 26258 madjusmdetlem4 30494 hgt750lemf 31333 hgt750leme 31338 circum 32165 itgmulc2nc 34103 pellexlem6 38358 pell1234qrmulcl 38379 rmxyadd 38445 wallispi2lem2 41216 dirkertrigeqlem3 41244 cevathlem1 41983 itsclc0xyqsolr 43505 |
Copyright terms: Public domain | W3C validator |