Theorem adddi 8301

Description: Alias for ax-distr 8273, for naming consistency with adddii 8326. (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 8273	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 1009   = wceq 1402   e. wcel 2209  (class class class)co 6075   CCcc 8167   + caddc 8172   x. cmul 8174

This theorem was proved from axioms:  ax-distr 8273

This theorem is referenced by:  adddir  8307  adddii  8326  adddid  8340  muladd11  8449  cnegex  8494  muladd  8701  nnmulcl  9304  expmul  10999  bernneq  11076  sqoddm1div8  11109  isermulc2  12084  efexp  12427  efi4p  12462  sinadd  12481  cosadd  12482  cos2tsin  12496  cos01bnd  12503  absefib  12516  efieq1re  12517  demoivreALT  12519  odd2np1  12618  opoe  12640  opeo  12642  gcdmultiple  12775  pythagtriplem12  13032  cncrng  14878  sinperlem  15832  2lgslem3d1  16133