![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnre | Unicode version |
Description: Alias for ax-cnre 7456, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 7456 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-cnre 7456 |
This theorem is referenced by: mulid1 7485 cnegexlem2 7658 cnegex 7660 apirr 8082 apsym 8083 apcotr 8084 apadd1 8085 apneg 8088 mulext1 8089 apti 8099 recexap 8122 creur 8419 creui 8420 cju 8421 cnref1o 9133 replim 10293 cjap 10340 |
Copyright terms: Public domain | W3C validator |