Theorem adddi 10025

Description: Alias for ax-distr 10003, for naming consistency with adddii 10050. (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 10003	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 1037   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939   x. cmul 9941

This theorem was proved from axioms:  ax-distr 10003

This theorem is referenced by:  adddir  10031  adddii  10050  adddid  10064  muladd11  10206  mul02lem1  10212  mul02  10214  muladd  10462  nnmulcl  11043  xadddilem  12124  expmul  12905  bernneq  12990  sqoddm1div8  13028  sqreulem  14099  isermulc2  14388  fsummulc2  14516  fsumcube  14791  efexp  14831  efi4p  14867  sinadd  14894  cosadd  14895  cos2tsin  14909  cos01bnd  14916  absefib  14928  efieq1re  14929  demoivreALT  14931  odd2np1  15065  opoe  15087  opeo  15089  gcdmultiple  15269  pythagtriplem12  15531  cncrng  19767  cnlmod  22940  plydivlem4  24051  sinperlem  24232  cxpsqrt  24449  chtub  24937  bcp1ctr  25004  2lgslem3d1  25128  cncvcOLD  27438  hhph  28035  2zrngALT  41948