Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cnre | Unicode version |
Description: Alias for ax-cnre 7699, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 7699 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 wcel 1465 wrex 2394 (class class class)co 5742 cc 7586 cr 7587 ci 7590 caddc 7591 cmul 7593 |
This theorem was proved from axioms: ax-cnre 7699 |
This theorem is referenced by: mulid1 7731 cnegexlem2 7906 cnegex 7908 apirr 8334 apsym 8335 apcotr 8336 apadd1 8337 apneg 8340 mulext1 8341 apti 8351 recexap 8381 creur 8681 creui 8682 cju 8683 cnref1o 9396 replim 10586 cjap 10633 |
Copyright terms: Public domain | W3C validator |