Theorem adddi 7535

Description: Alias for ax-distr 7510, for naming consistency with adddii 7559. (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 7510	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 925   = wceq 1290   e. wcel 1439  (class class class)co 5666   CCcc 7409   + caddc 7414   x. cmul 7416

This theorem was proved from axioms:  ax-distr 7510

This theorem is referenced by:  adddir  7540  adddii  7559  adddid  7573  muladd11  7676  cnegex  7721  muladd  7923  nnmulcl  8504  expmul  10061  bernneq  10135  sqoddm1div8  10167  iisermulc2  10789  efexp  11033  efi4p  11069  sinadd  11088  cosadd  11089  cos2tsin  11103  cos01bnd  11110  absefib  11121  efieq1re  11122  demoivreALT  11124  odd2np1  11212  opoe  11234  opeo  11236  gcdmultiple  11348