Theorem adddi 8142

Description: Alias for ax-distr 8114, for naming consistency with adddii 8167. (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 8114	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 1002   = wceq 1395   e. wcel 2200  (class class class)co 6007   CCcc 8008   + caddc 8013   x. cmul 8015

This theorem was proved from axioms:  ax-distr 8114

This theorem is referenced by:  adddir  8148  adddii  8167  adddid  8182  muladd11  8290  cnegex  8335  muladd  8541  nnmulcl  9142  expmul  10818  bernneq  10894  sqoddm1div8  10927  isermulc2  11866  efexp  12208  efi4p  12243  sinadd  12262  cosadd  12263  cos2tsin  12277  cos01bnd  12284  absefib  12297  efieq1re  12298  demoivreALT  12300  odd2np1  12399  opoe  12421  opeo  12423  gcdmultiple  12556  pythagtriplem12  12813  cncrng  14548  sinperlem  15497  2lgslem3d1  15794