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

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

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 10041 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054   = wceq 1523  wcel 2030  (class class class)co 6690  cc 9972   + caddc 9977   · cmul 9979
This theorem was proved from axioms:  ax-distr 10041
This theorem is referenced by:  adddir  10069  adddii  10088  adddid  10102  muladd11  10244  mul02lem1  10250  mul02  10252  muladd  10500  nnmulcl  11081  xadddilem  12162  expmul  12945  bernneq  13030  sqoddm1div8  13068  sqreulem  14143  isermulc2  14432  fsummulc2  14560  fsumcube  14835  efexp  14875  efi4p  14911  sinadd  14938  cosadd  14939  cos2tsin  14953  cos01bnd  14960  absefib  14972  efieq1re  14973  demoivreALT  14975  odd2np1  15112  opoe  15134  opeo  15136  gcdmultiple  15316  pythagtriplem12  15578  cncrng  19815  cnlmod  22986  plydivlem4  24096  sinperlem  24277  cxpsqrt  24494  chtub  24982  bcp1ctr  25049  2lgslem3d1  25173  cncvcOLD  27566  hhph  28163  2zrngALT  42273
  Copyright terms: Public domain W3C validator