Theorem adddi 8056

Description: Alias for ax-distr 8028, for naming consistency with adddii 8081. (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 8028	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 980   = wceq 1372   e. wcel 2175  (class class class)co 5943   CCcc 7922   + caddc 7927   x. cmul 7929

This theorem was proved from axioms:  ax-distr 8028

This theorem is referenced by:  adddir  8062  adddii  8081  adddid  8096  muladd11  8204  cnegex  8249  muladd  8455  nnmulcl  9056  expmul  10727  bernneq  10803  sqoddm1div8  10836  isermulc2  11622  efexp  11964  efi4p  11999  sinadd  12018  cosadd  12019  cos2tsin  12033  cos01bnd  12040  absefib  12053  efieq1re  12054  demoivreALT  12056  odd2np1  12155  opoe  12177  opeo  12179  gcdmultiple  12312  pythagtriplem12  12569  cncrng  14302  sinperlem  15251  2lgslem3d1  15548