![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adddi | Unicode version |
Description: Alias for ax-distr 7932, for naming consistency with adddii 7984. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 7932 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-distr 7932 |
This theorem is referenced by: adddir 7965 adddii 7984 adddid 7999 muladd11 8107 cnegex 8152 muladd 8358 nnmulcl 8957 expmul 10582 bernneq 10658 sqoddm1div8 10691 isermulc2 11365 efexp 11707 efi4p 11742 sinadd 11761 cosadd 11762 cos2tsin 11776 cos01bnd 11783 absefib 11795 efieq1re 11796 demoivreALT 11798 odd2np1 11895 opoe 11917 opeo 11919 gcdmultiple 12038 pythagtriplem12 12292 cncrng 13832 sinperlem 14612 |
Copyright terms: Public domain | W3C validator |