![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > adddi | Structured version Visualization version GIF version |
Description: Alias for ax-distr 11125, for naming consistency with adddii 11174. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi | โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))) |
Step | Hyp | Ref | 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 |