![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adddi | Unicode version |
Description: Alias for ax-distr 7449, for naming consistency with adddii 7498. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 7449 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-distr 7449 |
This theorem is referenced by: adddir 7479 adddii 7498 adddid 7512 muladd11 7615 cnegex 7660 muladd 7862 nnmulcl 8443 expmul 10000 bernneq 10074 sqoddm1div8 10106 iisermulc2 10728 efexp 10972 efi4p 11008 sinadd 11027 cosadd 11028 cos2tsin 11042 cos01bnd 11049 absefib 11060 efieq1re 11061 demoivreALT 11063 odd2np1 11151 opoe 11173 opeo 11175 gcdmultiple 11287 |
Copyright terms: Public domain | W3C validator |