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

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

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 7944 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 980   = wceq 1364  wcel 2160  (class class class)co 5895  cc 7838   + caddc 7843   · cmul 7845
This theorem was proved from axioms:  ax-distr 7944
This theorem is referenced by:  adddir  7977  adddii  7996  adddid  8011  muladd11  8119  cnegex  8164  muladd  8370  nnmulcl  8969  expmul  10595  bernneq  10671  sqoddm1div8  10704  isermulc2  11379  efexp  11721  efi4p  11756  sinadd  11775  cosadd  11776  cos2tsin  11790  cos01bnd  11797  absefib  11809  efieq1re  11810  demoivreALT  11812  odd2np1  11909  opoe  11931  opeo  11933  gcdmultiple  12052  pythagtriplem12  12306  cncrng  13869  sinperlem  14681
  Copyright terms: Public domain W3C validator