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

Theorem adddi 7745
Description: Alias for ax-distr 7717, for naming consistency with adddii 7769. (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 7717 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 962    = wceq 1331    e. wcel 1480  (class class class)co 5767   CCcc 7611    + caddc 7616    x. cmul 7618
This theorem was proved from axioms:  ax-distr 7717
This theorem is referenced by:  adddir  7750  adddii  7769  adddid  7783  muladd11  7888  cnegex  7933  muladd  8139  nnmulcl  8734  expmul  10331  bernneq  10405  sqoddm1div8  10437  isermulc2  11102  efexp  11377  efi4p  11413  sinadd  11432  cosadd  11433  cos2tsin  11447  cos01bnd  11454  absefib  11466  efieq1re  11467  demoivreALT  11469  odd2np1  11559  opoe  11581  opeo  11583  gcdmultiple  11697  sinperlem  12878
  Copyright terms: Public domain W3C validator