Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cnre | Unicode version |
Description: Alias for ax-cnre 6995, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 6995 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1243 wcel 1393 wrex 2307 (class class class)co 5512 cc 6887 cr 6888 ci 6891 caddc 6892 cmul 6894 |
This theorem was proved from axioms: ax-cnre 6995 |
This theorem is referenced by: mulid1 7024 cnegexlem2 7187 cnegex 7189 apirr 7596 apsym 7597 apcotr 7598 apadd1 7599 apneg 7602 mulext1 7603 apti 7613 recexap 7634 creur 7911 creui 7912 cju 7913 cnref1o 8582 replim 9459 cjap 9506 |
Copyright terms: Public domain | W3C validator |