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

Theorem adddi 7960
Description: Alias for ax-distr 7932, for naming consistency with adddii 7984. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
adddi  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 7932 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 979    = wceq 1363    e. wcel 2159  (class class class)co 5890   CCcc 7826    + caddc 7831    x. cmul 7833
This theorem was proved from axioms:  ax-distr 7932
This theorem is referenced by:  adddir  7965  adddii  7984  adddid  7999  muladd11  8107  cnegex  8152  muladd  8358  nnmulcl  8957  expmul  10582  bernneq  10658  sqoddm1div8  10691  isermulc2  11365  efexp  11707  efi4p  11742  sinadd  11761  cosadd  11762  cos2tsin  11776  cos01bnd  11783  absefib  11795  efieq1re  11796  demoivreALT  11798  odd2np1  11895  opoe  11917  opeo  11919  gcdmultiple  12038  pythagtriplem12  12292  cncrng  13832  sinperlem  14612
  Copyright terms: Public domain W3C validator