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

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

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 10592 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   + caddc 10528   · cmul 10530
This theorem was proved from axioms:  ax-distr 10592
This theorem is referenced by:  adddir  10620  adddii  10641  adddid  10653  muladd11  10798  mul02lem1  10804  mul02  10806  muladd  11060  nnmulcl  11649  xadddilem  12675  expmul  13462  bernneq  13578  sqoddm1div8  13592  sqreulem  14707  isermulc2  15002  fsummulc2  15127  fsumcube  15402  efexp  15442  efi4p  15478  sinadd  15505  cosadd  15506  cos2tsin  15520  cos01bnd  15527  absefib  15539  efieq1re  15540  demoivreALT  15542  odd2np1  15678  opoe  15700  opeo  15702  gcdmultipleOLD  15888  pythagtriplem12  16151  cncrng  20494  cnlmod  23671  plydivlem4  24812  sinperlem  24993  cxpsqrt  25213  chtub  25715  bcp1ctr  25782  2lgslem3d1  25906  cncvcOLD  28287  hhph  28882  2zrngALT  44147
  Copyright terms: Public domain W3C validator