Theorem adddi 8077

Description: Alias for ax-distr 8049, for naming consistency with adddii 8102. (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 8049	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 2177  (class class class)co 5957   CCcc 7943   + caddc 7948   x. cmul 7950

This theorem was proved from axioms:  ax-distr 8049

This theorem is referenced by:  adddir  8083  adddii  8102  adddid  8117  muladd11  8225  cnegex  8270  muladd  8476  nnmulcl  9077  expmul  10751  bernneq  10827  sqoddm1div8  10860  isermulc2  11726  efexp  12068  efi4p  12103  sinadd  12122  cosadd  12123  cos2tsin  12137  cos01bnd  12144  absefib  12157  efieq1re  12158  demoivreALT  12160  odd2np1  12259  opoe  12281  opeo  12283  gcdmultiple  12416  pythagtriplem12  12673  cncrng  14406  sinperlem  15355  2lgslem3d1  15652