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

Theorem adddid 6849
Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (φA ℂ)
addcld.2 (φB ℂ)
addassd.3 (φ𝐶 ℂ)
Assertion
Ref Expression
adddid (φ → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))

Proof of Theorem adddid
StepHypRef Expression
1 addcld.1 . 2 (φA ℂ)
2 addcld.2 . 2 (φB ℂ)
3 addassd.3 . 2 (φ𝐶 ℂ)
4 adddi 6811 . 2 ((A B 𝐶 ℂ) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))
51, 2, 3, 4syl3anc 1134 1 (φ → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242   wcel 1390  (class class class)co 5455  cc 6709   + caddc 6714   · cmul 6716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-distr 6787
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  subdi  7178  mulreim  7388  apadd1  7392  conjmulap  7487  cju  7694  binom2  9015  binom3  9019  remim  9088  mulreap  9092  readd  9097  remullem  9099  imadd  9105  cjadd  9112
  Copyright terms: Public domain W3C validator