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

Theorem adddi 7071
Description: Alias for ax-distr 7046, for naming consistency with adddii 7095. (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 7046 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 896    = wceq 1259    e. wcel 1409  (class class class)co 5540   CCcc 6945    + caddc 6950    x. cmul 6952
This theorem was proved from axioms:  ax-distr 7046
This theorem is referenced by:  adddir  7076  adddii  7095  adddid  7109  muladd11  7207  cnegex  7252  muladd  7453  nnmulcl  8011  expmul  9465  bernneq  9537  sqoddm1div8  9569  iisermulc2  10091  odd2np1  10184  opoe  10207  opeo  10209
  Copyright terms: Public domain W3C validator