Theorem adddi 7943

Description: Alias for ax-distr 7915, for naming consistency with adddii 7967. (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 7915	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 978   = wceq 1353   e. wcel 2148  (class class class)co 5875   CCcc 7809   + caddc 7814   x. cmul 7816

This theorem was proved from axioms:  ax-distr 7915

This theorem is referenced by:  adddir  7948  adddii  7967  adddid  7982  muladd11  8090  cnegex  8135  muladd  8341  nnmulcl  8940  expmul  10565  bernneq  10641  sqoddm1div8  10674  isermulc2  11348  efexp  11690  efi4p  11725  sinadd  11744  cosadd  11745  cos2tsin  11759  cos01bnd  11766  absefib  11778  efieq1re  11779  demoivreALT  11781  odd2np1  11878  opoe  11900  opeo  11902  gcdmultiple  12021  pythagtriplem12  12275  cncrng  13466  sinperlem  14232