Theorem adddi 8127

Description: Alias for ax-distr 8099, for naming consistency with adddii 8152. (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

Step	Hyp	Ref	Expression
1		ax-distr 8099	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )

Syntax hints:   -> wi 4   /\ w3a 1002   = wceq 1395   e. wcel 2200  (class class class)co 6000   CCcc 7993   + caddc 7998   x. cmul 8000

This theorem was proved from axioms:  ax-distr 8099

This theorem is referenced by:  adddir  8133  adddii  8152  adddid  8167  muladd11  8275  cnegex  8320  muladd  8526  nnmulcl  9127  expmul  10801  bernneq  10877  sqoddm1div8  10910  isermulc2  11846  efexp  12188  efi4p  12223  sinadd  12242  cosadd  12243  cos2tsin  12257  cos01bnd  12264  absefib  12277  efieq1re  12278  demoivreALT  12280  odd2np1  12379  opoe  12401  opeo  12403  gcdmultiple  12536  pythagtriplem12  12793  cncrng  14527  sinperlem  15476  2lgslem3d1  15773