Theorem adddi 7906

Description: Alias for ax-distr 7878, for naming consistency with adddii 7930. (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 7878	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 973   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   + caddc 7777   x. cmul 7779

This theorem was proved from axioms:  ax-distr 7878

This theorem is referenced by:  adddir  7911  adddii  7930  adddid  7944  muladd11  8052  cnegex  8097  muladd  8303  nnmulcl  8899  expmul  10521  bernneq  10596  sqoddm1div8  10629  isermulc2  11303  efexp  11645  efi4p  11680  sinadd  11699  cosadd  11700  cos2tsin  11714  cos01bnd  11721  absefib  11733  efieq1re  11734  demoivreALT  11736  odd2np1  11832  opoe  11854  opeo  11856  gcdmultiple  11975  pythagtriplem12  12229  sinperlem  13523