Theorem adddi 8154

Description: Alias for ax-distr 8126, for naming consistency with adddii 8179. (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 8126	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 6013   CCcc 8020   + caddc 8025   x. cmul 8027

This theorem was proved from axioms:  ax-distr 8126

This theorem is referenced by:  adddir  8160  adddii  8179  adddid  8194  muladd11  8302  cnegex  8347  muladd  8553  nnmulcl  9154  expmul  10836  bernneq  10912  sqoddm1div8  10945  isermulc2  11891  efexp  12233  efi4p  12268  sinadd  12287  cosadd  12288  cos2tsin  12302  cos01bnd  12309  absefib  12322  efieq1re  12323  demoivreALT  12325  odd2np1  12424  opoe  12446  opeo  12448  gcdmultiple  12581  pythagtriplem12  12838  cncrng  14573  sinperlem  15522  2lgslem3d1  15819