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

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

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 11222 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087   = wceq 1540  wcel 2108  (class class class)co 7431  cc 11153   + caddc 11158   · cmul 11160
This theorem was proved from axioms:  ax-distr 11222
This theorem is referenced by:  adddir  11252  adddii  11273  adddid  11285  muladd11  11431  mul02lem1  11437  mul02  11439  muladd  11695  nnmulcl  12290  xadddilem  13336  expmul  14148  bernneq  14268  sqoddm1div8  14282  sqreulem  15398  isermulc2  15694  fsummulc2  15820  fsumcube  16096  efexp  16137  efi4p  16173  sinadd  16200  cosadd  16201  cos2tsin  16215  cos01bnd  16222  absefib  16234  efieq1re  16235  demoivreALT  16237  odd2np1  16378  opoe  16400  opeo  16402  pythagtriplem12  16864  cncrng  21401  cncrngOLD  21402  cnlmod  25173  plydivlem4  26338  sinperlem  26522  cxpsqrt  26745  chtub  27256  bcp1ctr  27323  2lgslem3d1  27447  cncvcOLD  30602  hhph  31197  2zrngALT  48170
  Copyright terms: Public domain W3C validator