Theorem adddi 7752

Description: Alias for ax-distr 7724, for naming consistency with adddii 7776. (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 7724	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 962   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   + caddc 7623   x. cmul 7625

This theorem was proved from axioms:  ax-distr 7724

This theorem is referenced by:  adddir  7757  adddii  7776  adddid  7790  muladd11  7895  cnegex  7940  muladd  8146  nnmulcl  8741  expmul  10338  bernneq  10412  sqoddm1div8  10444  isermulc2  11109  efexp  11388  efi4p  11424  sinadd  11443  cosadd  11444  cos2tsin  11458  cos01bnd  11465  absefib  11477  efieq1re  11478  demoivreALT  11480  odd2np1  11570  opoe  11592  opeo  11594  gcdmultiple  11708  sinperlem  12889