Theorem adddi 7474

Description: Alias for ax-distr 7449, for naming consistency with adddii 7498. (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 7449	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 924   = wceq 1289   e. wcel 1438  (class class class)co 5652   CCcc 7348   + caddc 7353   x. cmul 7355

This theorem was proved from axioms:  ax-distr 7449

This theorem is referenced by:  adddir  7479  adddii  7498  adddid  7512  muladd11  7615  cnegex  7660  muladd  7862  nnmulcl  8443  expmul  10000  bernneq  10074  sqoddm1div8  10106  iisermulc2  10728  efexp  10972  efi4p  11008  sinadd  11027  cosadd  11028  cos2tsin  11042  cos01bnd  11049  absefib  11060  efieq1re  11061  demoivreALT  11063  odd2np1  11151  opoe  11173  opeo  11175  gcdmultiple  11287