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

Theorem adddi 7877
Description: Alias for ax-distr 7849, for naming consistency with adddii 7901. (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 7849 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 967    = wceq 1342    e. wcel 2135  (class class class)co 5837   CCcc 7743    + caddc 7748    x. cmul 7750
This theorem was proved from axioms:  ax-distr 7849
This theorem is referenced by:  adddir  7882  adddii  7901  adddid  7915  muladd11  8023  cnegex  8068  muladd  8274  nnmulcl  8870  expmul  10491  bernneq  10565  sqoddm1div8  10598  isermulc2  11271  efexp  11613  efi4p  11648  sinadd  11667  cosadd  11668  cos2tsin  11682  cos01bnd  11689  absefib  11701  efieq1re  11702  demoivreALT  11704  odd2np1  11799  opoe  11821  opeo  11823  gcdmultiple  11942  pythagtriplem12  12196  sinperlem  13296
  Copyright terms: Public domain W3C validator