Theorem adddi 7776

Description: Alias for ax-distr 7748, for naming consistency with adddii 7800. (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 7748	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 963   = wceq 1332   e. wcel 1481  (class class class)co 5782   CCcc 7642   + caddc 7647   x. cmul 7649

This theorem was proved from axioms:  ax-distr 7748

This theorem is referenced by:  adddir  7781  adddii  7800  adddid  7814  muladd11  7919  cnegex  7964  muladd  8170  nnmulcl  8765  expmul  10369  bernneq  10443  sqoddm1div8  10475  isermulc2  11141  efexp  11425  efi4p  11460  sinadd  11479  cosadd  11480  cos2tsin  11494  cos01bnd  11501  absefib  11513  efieq1re  11514  demoivreALT  11516  odd2np1  11606  opoe  11628  opeo  11630  gcdmultiple  11744  sinperlem  12937