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

Theorem adddi 7474
Description: Alias for ax-distr 7449, for naming consistency with adddii 7498. (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 7449 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 924    = wceq 1289    e. wcel 1438  (class class class)co 5652   CCcc 7348    + caddc 7353    x. cmul 7355
This theorem was proved from axioms:  ax-distr 7449
This theorem is referenced by:  adddir  7479  adddii  7498  adddid  7512  muladd11  7615  cnegex  7660  muladd  7862  nnmulcl  8443  expmul  10000  bernneq  10074  sqoddm1div8  10106  iisermulc2  10728  efexp  10972  efi4p  11008  sinadd  11027  cosadd  11028  cos2tsin  11042  cos01bnd  11049  absefib  11060  efieq1re  11061  demoivreALT  11063  odd2np1  11151  opoe  11173  opeo  11175  gcdmultiple  11287
  Copyright terms: Public domain W3C validator