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  11041  bernneq  11118  sqoddm1div8  11151  isermulc2  12130  efexp  12473  efi4p  12508  sinadd  12527  cosadd  12528  cos2tsin  12542  cos01bnd  12549  absefib  12562  efieq1re  12563  demoivreALT  12565  odd2np1  12664  opoe  12686  opeo  12688  gcdmultiple  12821  pythagtriplem12  13082  cncrng  15014  sinperlem  16052  chtqub  16313  bcp1ctr  16323  2lgslem3d1  16441