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

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

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 7142 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920   = wceq 1285  wcel 1434  (class class class)co 5543  cc 7041   + caddc 7046   · cmul 7048
This theorem was proved from axioms:  ax-distr 7142
This theorem is referenced by:  adddir  7172  adddii  7191  adddid  7205  muladd11  7308  cnegex  7353  muladd  7555  nnmulcl  8127  expmul  9618  bernneq  9690  sqoddm1div8  9722  iisermulc2  10316  odd2np1  10417  opoe  10439  opeo  10441  gcdmultiple  10553
  Copyright terms: Public domain W3C validator