Theorem adddi 8164

Description: Alias for ax-distr 8136, for naming consistency with adddii 8189. (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 8136	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 1004   = wceq 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   + caddc 8035   x. cmul 8037

This theorem was proved from axioms:  ax-distr 8136

This theorem is referenced by:  adddir  8170  adddii  8189  adddid  8204  muladd11  8312  cnegex  8357  muladd  8563  nnmulcl  9164  expmul  10847  bernneq  10923  sqoddm1div8  10956  isermulc2  11918  efexp  12261  efi4p  12296  sinadd  12315  cosadd  12316  cos2tsin  12330  cos01bnd  12337  absefib  12350  efieq1re  12351  demoivreALT  12353  odd2np1  12452  opoe  12474  opeo  12476  gcdmultiple  12609  pythagtriplem12  12866  cncrng  14602  sinperlem  15551  2lgslem3d1  15848