![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnre | Unicode version |
Description: Alias for ax-cnre 7900, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 7900 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-cnre 7900 |
This theorem is referenced by: mulid1 7932 cnegexlem2 8110 cnegex 8112 apirr 8539 apsym 8540 apcotr 8541 apadd1 8542 apneg 8545 mulext1 8546 apti 8556 recexap 8586 creur 8892 creui 8893 cju 8894 cnref1o 9626 replim 10839 cjap 10886 |
Copyright terms: Public domain | W3C validator |