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

Theorem adddid 7982
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 7943 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4syl3anc 1238 1  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353    e. wcel 2148  (class class class)co 5875   CCcc 7809    + caddc 7814    x. cmul 7816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-distr 7915
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  subdi  8342  mulreim  8561  apadd1  8565  conjmulap  8686  cju  8918  flhalf  10302  modqcyc  10359  addmodlteq  10398  binom2  10632  binom3  10638  sqoddm1div8  10674  bcpasc  10746  remim  10869  mulreap  10873  readd  10878  remullem  10880  imadd  10886  cjadd  10893  bdtrilem  11247  fsummulc2  11456  binomlem  11491  tanval3ap  11722  sinadd  11744  tanaddap  11747  bezoutlemnewy  11997  dvdsmulgcd  12026  lcmgcdlem  12077  pythagtriplem1  12265  pcaddlem  12338  mul4sqlem  12391  tangtx  14262  rpmulcxp  14333  binom4  14400  lgseisenlem2  14454  2lgsoddprmlem2  14457  2sqlem4  14468  2sqlem8  14473
  Copyright terms: Public domain W3C validator