Theorem adddi 8004

Description: Alias for ax-distr 7976, for naming consistency with adddii 8029. (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 7976	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 980   = wceq 1364   e. wcel 2164  (class class class)co 5918   CCcc 7870   + caddc 7875   x. cmul 7877

This theorem was proved from axioms:  ax-distr 7976

This theorem is referenced by:  adddir  8010  adddii  8029  adddid  8044  muladd11  8152  cnegex  8197  muladd  8403  nnmulcl  9003  expmul  10655  bernneq  10731  sqoddm1div8  10764  isermulc2  11483  efexp  11825  efi4p  11860  sinadd  11879  cosadd  11880  cos2tsin  11894  cos01bnd  11901  absefib  11914  efieq1re  11915  demoivreALT  11917  odd2np1  12014  opoe  12036  opeo  12038  gcdmultiple  12157  pythagtriplem12  12413  cncrng  14057  sinperlem  14943