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  8460  cnegex  8505  muladd  8712  nnmulcl  9327  expmul  11034  bernneq  11111  sqoddm1div8  11144  isermulc2  12122  efexp  12465  efi4p  12500  sinadd  12519  cosadd  12520  cos2tsin  12534  cos01bnd  12541  absefib  12554  efieq1re  12555  demoivreALT  12557  odd2np1  12656  opoe  12678  opeo  12680  gcdmultiple  12813  pythagtriplem12  13074  cncrng  14955  sinperlem  15959  bcp1ctr  16204  2lgslem3d1  16317