Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  adddi GIF version

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

StepHypRef Expression
1 ax-distr 7717 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 962   = wceq 1331   ∈ wcel 1480  (class class class)co 5767  ℂcc 7611   + caddc 7616   · cmul 7618 This theorem was proved from axioms:  ax-distr 7717 This theorem is referenced by:  adddir  7750  adddii  7769  adddid  7783  muladd11  7888  cnegex  7933  muladd  8139  nnmulcl  8734  expmul  10331  bernneq  10405  sqoddm1div8  10437  isermulc2  11102  efexp  11377  efi4p  11413  sinadd  11432  cosadd  11433  cos2tsin  11447  cos01bnd  11454  absefib  11466  efieq1re  11467  demoivreALT  11469  odd2np1  11559  opoe  11581  opeo  11583  gcdmultiple  11697  sinperlem  12878
 Copyright terms: Public domain W3C validator