MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adddi Structured version   Visualization version   GIF version

Theorem adddi 10615
Description: Alias for ax-distr 10593, for naming consistency with adddii 10642. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
adddi ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 10593 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1538  wcel 2114  (class class class)co 7140  cc 10524   + caddc 10529   · cmul 10531
This theorem was proved from axioms:  ax-distr 10593
This theorem is referenced by:  adddir  10621  adddii  10642  adddid  10654  muladd11  10799  mul02lem1  10805  mul02  10807  muladd  11061  nnmulcl  11649  xadddilem  12675  expmul  13470  bernneq  13586  sqoddm1div8  13600  sqreulem  14710  isermulc2  15005  fsummulc2  15130  fsumcube  15405  efexp  15445  efi4p  15481  sinadd  15508  cosadd  15509  cos2tsin  15523  cos01bnd  15530  absefib  15542  efieq1re  15543  demoivreALT  15545  odd2np1  15681  opoe  15703  opeo  15705  gcdmultipleOLD  15889  pythagtriplem12  16152  cncrng  20110  cnlmod  23743  plydivlem4  24890  sinperlem  25071  cxpsqrt  25292  chtub  25794  bcp1ctr  25861  2lgslem3d1  25985  cncvcOLD  28364  hhph  28959  2zrngALT  44512
  Copyright terms: Public domain W3C validator