Theorem adddi 7960

Description: Alias for ax-distr 7932, for naming consistency with adddii 7984. (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 7932	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 979   = wceq 1363   e. wcel 2159  (class class class)co 5890   CCcc 7826   + caddc 7831   x. cmul 7833

This theorem was proved from axioms:  ax-distr 7932

This theorem is referenced by:  adddir  7965  adddii  7984  adddid  7999  muladd11  8107  cnegex  8152  muladd  8358  nnmulcl  8957  expmul  10582  bernneq  10658  sqoddm1div8  10691  isermulc2  11365  efexp  11707  efi4p  11742  sinadd  11761  cosadd  11762  cos2tsin  11776  cos01bnd  11783  absefib  11795  efieq1re  11796  demoivreALT  11798  odd2np1  11895  opoe  11917  opeo  11919  gcdmultiple  12038  pythagtriplem12  12292  cncrng  13832  sinperlem  14612