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

Theorem adddi 11147
Description: Alias for ax-distr 11125, for naming consistency with adddii 11174. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
adddi ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 11125 1 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7362  โ„‚cc 11056   + caddc 11061   ยท cmul 11063
This theorem was proved from axioms:  ax-distr 11125
This theorem is referenced by:  adddir  11153  adddii  11174  adddid  11186  muladd11  11332  mul02lem1  11338  mul02  11340  muladd  11594  nnmulcl  12184  xadddilem  13220  expmul  14020  bernneq  14139  sqoddm1div8  14153  sqreulem  15251  isermulc2  15549  fsummulc2  15676  fsumcube  15950  efexp  15990  efi4p  16026  sinadd  16053  cosadd  16054  cos2tsin  16068  cos01bnd  16075  absefib  16087  efieq1re  16088  demoivreALT  16090  odd2np1  16230  opoe  16252  opeo  16254  pythagtriplem12  16705  cncrng  20834  cnlmod  24519  plydivlem4  25672  sinperlem  25853  cxpsqrt  26074  chtub  26576  bcp1ctr  26643  2lgslem3d1  26767  cncvcOLD  29567  hhph  30162  2zrngALT  46320
  Copyright terms: Public domain W3C validator