Theorem adddi 8312

Description: Alias for ax-distr 8284, for naming consistency with adddii 8337. (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 8284	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 8178   + caddc 8183   x. cmul 8185

This proof depends on axioms:  ax-distr 8284

This theorem is used by:  adddir  8318  adddii  8337  adddid  8351  muladd11  8461  cnegex  8506  muladd  8713  nnmulcl  9328  expmul  11036  bernneq  11113  sqoddm1div8  11146  isermulc2  12125  efexp  12468  efi4p  12503  sinadd  12522  cosadd  12523  cos2tsin  12537  cos01bnd  12544  absefib  12557  efieq1re  12558  demoivreALT  12560  odd2np1  12659  opoe  12681  opeo  12683  gcdmultiple  12816  pythagtriplem12  13077  cncrng  14990  sinperlem  16001  chtqub  16257  bcp1ctr  16267  2lgslem3d1  16385