Theorem adddi 11242

Description: Alias for ax-distr 11220, for naming consistency with adddii 11271. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
adddi	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddi

Step	Hyp	Ref	Expression
1		ax-distr 11220	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151   + caddc 11156   · cmul 11158

This theorem was proved from axioms:  ax-distr 11220

This theorem is referenced by:  adddir  11250  adddii  11271  adddid  11283  muladd11  11429  mul02lem1  11435  mul02  11437  muladd  11693  nnmulcl  12288  xadddilem  13333  expmul  14145  bernneq  14265  sqoddm1div8  14279  sqreulem  15395  isermulc2  15691  fsummulc2  15817  fsumcube  16093  efexp  16134  efi4p  16170  sinadd  16197  cosadd  16198  cos2tsin  16212  cos01bnd  16219  absefib  16231  efieq1re  16232  demoivreALT  16234  odd2np1  16375  opoe  16397  opeo  16399  pythagtriplem12  16860  cncrng  21419  cncrngOLD  21420  cnlmod  25187  plydivlem4  26353  sinperlem  26537  cxpsqrt  26760  chtub  27271  bcp1ctr  27338  2lgslem3d1  27462  cncvcOLD  30612  hhph  31207  2zrngALT  48098