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

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

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 7865 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 973   = wceq 1348  wcel 2141  (class class class)co 5850  cc 7759   + caddc 7764   · cmul 7766
This theorem was proved from axioms:  ax-distr 7865
This theorem is referenced by:  adddir  7898  adddii  7917  adddid  7931  muladd11  8039  cnegex  8084  muladd  8290  nnmulcl  8886  expmul  10508  bernneq  10583  sqoddm1div8  10616  isermulc2  11290  efexp  11632  efi4p  11667  sinadd  11686  cosadd  11687  cos2tsin  11701  cos01bnd  11708  absefib  11720  efieq1re  11721  demoivreALT  11723  odd2np1  11819  opoe  11841  opeo  11843  gcdmultiple  11962  pythagtriplem12  12216  sinperlem  13482
  Copyright terms: Public domain W3C validator