Theorem adddi 8057

Description: Alias for ax-distr 8029, for naming consistency with adddii 8082. (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 8029	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 981   = wceq 1373   e. wcel 2176  (class class class)co 5944   CCcc 7923   + caddc 7928   x. cmul 7930

This theorem was proved from axioms:  ax-distr 8029

This theorem is referenced by:  adddir  8063  adddii  8082  adddid  8097  muladd11  8205  cnegex  8250  muladd  8456  nnmulcl  9057  expmul  10729  bernneq  10805  sqoddm1div8  10838  isermulc2  11651  efexp  11993  efi4p  12028  sinadd  12047  cosadd  12048  cos2tsin  12062  cos01bnd  12069  absefib  12082  efieq1re  12083  demoivreALT  12085  odd2np1  12184  opoe  12206  opeo  12208  gcdmultiple  12341  pythagtriplem12  12598  cncrng  14331  sinperlem  15280  2lgslem3d1  15577