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

Theorem adddid 7758
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 7720 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4syl3anc 1201 1  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316    e. wcel 1465  (class class class)co 5742   CCcc 7586    + caddc 7591    x. cmul 7593
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 7692
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  subdi  8115  mulreim  8334  apadd1  8338  conjmulap  8457  cju  8687  flhalf  10043  modqcyc  10100  addmodlteq  10139  binom2  10371  binom3  10377  sqoddm1div8  10412  bcpasc  10480  remim  10600  mulreap  10604  readd  10609  remullem  10611  imadd  10617  cjadd  10624  bdtrilem  10978  fsummulc2  11185  binomlem  11220  tanval3ap  11348  sinadd  11370  tanaddap  11373  bezoutlemnewy  11611  dvdsmulgcd  11640  lcmgcdlem  11685  tangtx  12846
  Copyright terms: Public domain W3C validator