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

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

Proof of Theorem adddi
StepHypRef 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