Theorem adddi 7881

Description: Alias for ax-distr 7853, for naming consistency with adddii 7905. (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 7853	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 968   = wceq 1343   e. wcel 2136  (class class class)co 5841   CCcc 7747   + caddc 7752   x. cmul 7754

This theorem was proved from axioms:  ax-distr 7853

This theorem is referenced by:  adddir  7886  adddii  7905  adddid  7919  muladd11  8027  cnegex  8072  muladd  8278  nnmulcl  8874  expmul  10496  bernneq  10571  sqoddm1div8  10604  isermulc2  11277  efexp  11619  efi4p  11654  sinadd  11673  cosadd  11674  cos2tsin  11688  cos01bnd  11695  absefib  11707  efieq1re  11708  demoivreALT  11710  odd2np1  11806  opoe  11828  opeo  11830  gcdmultiple  11949  pythagtriplem12  12203  sinperlem  13329