![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > adddi | Structured version Visualization version GIF version |
Description: Alias for ax-distr 11052, for naming consistency with adddii 11101. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 11052 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 (class class class)co 7350 ℂcc 10983 + caddc 10988 · cmul 10990 |
This theorem was proved from axioms: ax-distr 11052 |
This theorem is referenced by: adddir 11080 adddii 11101 adddid 11113 muladd11 11259 mul02lem1 11265 mul02 11267 muladd 11521 nnmulcl 12111 xadddilem 13143 expmul 13943 bernneq 14059 sqoddm1div8 14073 sqreulem 15180 isermulc2 15478 fsummulc2 15605 fsumcube 15879 efexp 15919 efi4p 15955 sinadd 15982 cosadd 15983 cos2tsin 15997 cos01bnd 16004 absefib 16016 efieq1re 16017 demoivreALT 16019 odd2np1 16159 opoe 16181 opeo 16183 pythagtriplem12 16634 cncrng 20747 cnlmod 24431 plydivlem4 25584 sinperlem 25765 cxpsqrt 25986 chtub 26488 bcp1ctr 26555 2lgslem3d1 26679 cncvcOLD 29330 hhph 29925 2zrngALT 46037 |
Copyright terms: Public domain | W3C validator |