Theorem adddi 8311

Description: Alias for ax-distr 8283, for naming consistency with adddii 8336. (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 8283	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8177   + caddc 8182   x. cmul 8184

This proof depends on axioms:  ax-distr 8283

This theorem is used by:  adddir  8317  adddii  8336  adddid  8350  muladd11  8459  cnegex  8504  muladd  8711  nnmulcl  9325  expmul  11021  bernneq  11098  sqoddm1div8  11131  isermulc2  12106  efexp  12449  efi4p  12484  sinadd  12503  cosadd  12504  cos2tsin  12518  cos01bnd  12525  absefib  12538  efieq1re  12539  demoivreALT  12541  odd2np1  12640  opoe  12662  opeo  12664  gcdmultiple  12797  pythagtriplem12  13054  cncrng  14906  sinperlem  15909  2lgslem3d1  16219