MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adddi Structured version   Visualization version   GIF version

Theorem adddi 9970
Description: Alias for ax-distr 9948, for naming consistency with adddii 9995. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
adddi ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 9948 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036   = wceq 1480  wcel 1992  (class class class)co 6605  cc 9879   + caddc 9884   · cmul 9886
This theorem was proved from axioms:  ax-distr 9948
This theorem is referenced by:  adddir  9976  adddii  9995  adddid  10009  muladd11  10151  mul02lem1  10157  mul02  10159  muladd  10407  nnmulcl  10988  xadddilem  12064  expmul  12842  bernneq  12927  sqoddm1div8  12965  sqreulem  14028  isermulc2  14317  fsummulc2  14439  fsumcube  14711  efexp  14751  efi4p  14787  sinadd  14814  cosadd  14815  cos2tsin  14829  cos01bnd  14836  absefib  14848  efieq1re  14849  demoivreALT  14851  odd2np1  14984  opoe  15006  opeo  15008  gcdmultiple  15188  pythagtriplem12  15450  cncrng  19681  cnlmod  22843  plydivlem4  23950  sinperlem  24131  cxpsqrt  24344  chtub  24832  bcp1ctr  24899  2lgslem3d1  25023  cncvcOLD  27278  hhph  27875  2zrngALT  41209
  Copyright terms: Public domain W3C validator