Theorem adddi 8207

Description: Alias for ax-distr 8179, for naming consistency with adddii 8232. (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 8179	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 2202  (class class class)co 6028   CCcc 8073   + caddc 8078   x. cmul 8080

This theorem was proved from axioms:  ax-distr 8179

This theorem is referenced by:  adddir  8213  adddii  8232  adddid  8246  muladd11  8354  cnegex  8399  muladd  8605  nnmulcl  9206  expmul  10892  bernneq  10968  sqoddm1div8  11001  isermulc2  11963  efexp  12306  efi4p  12341  sinadd  12360  cosadd  12361  cos2tsin  12375  cos01bnd  12382  absefib  12395  efieq1re  12396  demoivreALT  12398  odd2np1  12497  opoe  12519  opeo  12521  gcdmultiple  12654  pythagtriplem12  12911  cncrng  14648  sinperlem  15602  2lgslem3d1  15902