Theorem adddi 8163

Description: Alias for ax-distr 8135, for naming consistency with adddii 8188. (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 8135	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 1004   = wceq 1397   e. wcel 2202  (class class class)co 6017   CCcc 8029   + caddc 8034   x. cmul 8036

This theorem was proved from axioms:  ax-distr 8135

This theorem is referenced by:  adddir  8169  adddii  8188  adddid  8203  muladd11  8311  cnegex  8356  muladd  8562  nnmulcl  9163  expmul  10845  bernneq  10921  sqoddm1div8  10954  isermulc2  11900  efexp  12242  efi4p  12277  sinadd  12296  cosadd  12297  cos2tsin  12311  cos01bnd  12318  absefib  12331  efieq1re  12332  demoivreALT  12334  odd2np1  12433  opoe  12455  opeo  12457  gcdmultiple  12590  pythagtriplem12  12847  cncrng  14582  sinperlem  15531  2lgslem3d1  15828