Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adddi | Unicode version |
Description: Alias for ax-distr 7849, for naming consistency with adddii 7901. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 7849 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 967 wceq 1342 wcel 2135 (class class class)co 5837 cc 7743 caddc 7748 cmul 7750 |
This theorem was proved from axioms: ax-distr 7849 |
This theorem is referenced by: adddir 7882 adddii 7901 adddid 7915 muladd11 8023 cnegex 8068 muladd 8274 nnmulcl 8870 expmul 10491 bernneq 10565 sqoddm1div8 10598 isermulc2 11271 efexp 11613 efi4p 11648 sinadd 11667 cosadd 11668 cos2tsin 11682 cos01bnd 11689 absefib 11701 efieq1re 11702 demoivreALT 11704 odd2np1 11799 opoe 11821 opeo 11823 gcdmultiple 11942 pythagtriplem12 12196 sinperlem 13296 |
Copyright terms: Public domain | W3C validator |