![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnre | Unicode version |
Description: Alias for ax-cnre 7755, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 7755 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-cnre 7755 |
This theorem is referenced by: mulid1 7787 cnegexlem2 7962 cnegex 7964 apirr 8391 apsym 8392 apcotr 8393 apadd1 8394 apneg 8397 mulext1 8398 apti 8408 recexap 8438 creur 8741 creui 8742 cju 8743 cnref1o 9469 replim 10663 cjap 10710 |
Copyright terms: Public domain | W3C validator |