Theorem adddi 8275

Description: Alias for ax-distr 8247, for naming consistency with adddii 8300. (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 8247	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 1005   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   + caddc 8146   x. cmul 8148

This theorem was proved from axioms:  ax-distr 8247

This theorem is referenced by:  adddir  8281  adddii  8300  adddid  8314  muladd11  8422  cnegex  8467  muladd  8674  nnmulcl  9275  expmul  10970  bernneq  11047  sqoddm1div8  11080  isermulc2  12050  efexp  12393  efi4p  12428  sinadd  12447  cosadd  12448  cos2tsin  12462  cos01bnd  12469  absefib  12482  efieq1re  12483  demoivreALT  12485  odd2np1  12584  opoe  12606  opeo  12608  gcdmultiple  12741  pythagtriplem12  12998  cncrng  14843  sinperlem  15799  2lgslem3d1  16099