Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adddi | Unicode version |
Description: Alias for ax-distr 7724, for naming consistency with adddii 7776. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 7724 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 962 wceq 1331 wcel 1480 (class class class)co 5774 cc 7618 caddc 7623 cmul 7625 |
This theorem was proved from axioms: ax-distr 7724 |
This theorem is referenced by: adddir 7757 adddii 7776 adddid 7790 muladd11 7895 cnegex 7940 muladd 8146 nnmulcl 8741 expmul 10338 bernneq 10412 sqoddm1div8 10444 isermulc2 11109 efexp 11388 efi4p 11424 sinadd 11443 cosadd 11444 cos2tsin 11458 cos01bnd 11465 absefib 11477 efieq1re 11478 demoivreALT 11480 odd2np1 11570 opoe 11592 opeo 11594 gcdmultiple 11708 sinperlem 12889 |
Copyright terms: Public domain | W3C validator |