Theorem adddi 8259

Description: Alias for ax-distr 8231, for naming consistency with adddii 8284. (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 8231	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 1005   = wceq 1398   e. wcel 2203  (class class class)co 6050   CCcc 8125   + caddc 8130   x. cmul 8132

This theorem was proved from axioms:  ax-distr 8231

This theorem is referenced by:  adddir  8265  adddii  8284  adddid  8298  muladd11  8406  cnegex  8451  muladd  8657  nnmulcl  9258  expmul  10946  bernneq  11022  sqoddm1div8  11055  isermulc2  12025  efexp  12368  efi4p  12403  sinadd  12422  cosadd  12423  cos2tsin  12437  cos01bnd  12444  absefib  12457  efieq1re  12458  demoivreALT  12460  odd2np1  12559  opoe  12581  opeo  12583  gcdmultiple  12716  pythagtriplem12  12973  cncrng  14717  sinperlem  15673  2lgslem3d1  15973