Theorem adddi 8092

Description: Alias for ax-distr 8064, for naming consistency with adddii 8117. (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 8064	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 981   = wceq 1373   e. wcel 2178  (class class class)co 5967   CCcc 7958   + caddc 7963   x. cmul 7965

This theorem was proved from axioms:  ax-distr 8064

This theorem is referenced by:  adddir  8098  adddii  8117  adddid  8132  muladd11  8240  cnegex  8285  muladd  8491  nnmulcl  9092  expmul  10766  bernneq  10842  sqoddm1div8  10875  isermulc2  11766  efexp  12108  efi4p  12143  sinadd  12162  cosadd  12163  cos2tsin  12177  cos01bnd  12184  absefib  12197  efieq1re  12198  demoivreALT  12200  odd2np1  12299  opoe  12321  opeo  12323  gcdmultiple  12456  pythagtriplem12  12713  cncrng  14446  sinperlem  15395  2lgslem3d1  15692