Theorem adddi 8317

Description: Alias for ax-distr 8289, for naming consistency with adddii 8342. (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 8289	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 6088   CCcc 8183   + caddc 8188   x. cmul 8190

This proof depends on axioms:  ax-distr 8289

This theorem is used by:  adddir  8323  adddii  8342  adddid  8356  muladd11  8466  cnegex  8511  muladd  8718  nnmulcl  9334  expmul  11042  bernneq  11119  sqoddm1div8  11152  isermulc2  12131  efexp  12474  efi4p  12509  sinadd  12528  cosadd  12529  cos2tsin  12543  cos01bnd  12550  absefib  12563  efieq1re  12564  demoivreALT  12566  odd2np1  12665  opoe  12687  opeo  12689  gcdmultiple  12822  pythagtriplem12  13083  cncrng  15015  sinperlem  16035  chtqub  16296  bcp1ctr  16306  2lgslem3d1  16424