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

Theorem adddid 7257
Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
addassd.3  |-  ( ph  ->  C  e.  CC )
Assertion
Ref Expression
adddid  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )

Proof of Theorem adddid
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addassd.3 . 2  |-  ( ph  ->  C  e.  CC )
4 adddi 7219 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4syl3anc 1170 1  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285    e. wcel 1434  (class class class)co 5563   CCcc 7093    + caddc 7098    x. cmul 7100
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-distr 7194
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  subdi  7608  mulreim  7823  apadd1  7827  conjmulap  7936  cju  8157  flhalf  9436  modqcyc  9493  addmodlteq  9532  binom2  9734  binom3  9739  sqoddm1div8  9774  bcpasc  9842  remim  9948  mulreap  9952  readd  9957  remullem  9959  imadd  9965  cjadd  9972  bezoutlemnewy  10592  dvdsmulgcd  10621  lcmgcdlem  10666
  Copyright terms: Public domain W3C validator