Theorem adddi 11157

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071   · cmul 11073

This theorem was proved from axioms:  ax-distr 11135

This theorem is referenced by:  adddir  11165  adddii  11186  adddid  11198  muladd11  11344  mul02lem1  11350  mul02  11352  muladd  11610  nnmulcl  12210  xadddilem  13254  expmul  14072  bernneq  14194  sqoddm1div8  14208  sqreulem  15326  isermulc2  15624  fsummulc2  15750  fsumcube  16026  efexp  16069  efi4p  16105  sinadd  16132  cosadd  16133  cos2tsin  16147  cos01bnd  16154  absefib  16166  efieq1re  16167  demoivreALT  16169  odd2np1  16311  opoe  16333  opeo  16335  pythagtriplem12  16797  cncrng  21300  cncrngOLD  21301  cnlmod  25040  plydivlem4  26204  sinperlem  26389  cxpsqrt  26612  chtub  27123  bcp1ctr  27190  2lgslem3d1  27314  cncvcOLD  30512  hhph  31107  2zrngALT  48242