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

Theorem adddid 7790
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 7752 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4syl3anc 1216 1  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331    e. wcel 1480  (class class class)co 5774   CCcc 7618    + caddc 7623    x. cmul 7625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-distr 7724
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  subdi  8147  mulreim  8366  apadd1  8370  conjmulap  8489  cju  8719  flhalf  10075  modqcyc  10132  addmodlteq  10171  binom2  10403  binom3  10409  sqoddm1div8  10444  bcpasc  10512  remim  10632  mulreap  10636  readd  10641  remullem  10643  imadd  10649  cjadd  10656  bdtrilem  11010  fsummulc2  11217  binomlem  11252  tanval3ap  11421  sinadd  11443  tanaddap  11446  bezoutlemnewy  11684  dvdsmulgcd  11713  lcmgcdlem  11758  tangtx  12919
  Copyright terms: Public domain W3C validator