![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnre | Unicode version |
Description: Alias for ax-cnre 7517, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
cnre |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnre 7517 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-cnre 7517 |
This theorem is referenced by: mulid1 7546 cnegexlem2 7719 cnegex 7721 apirr 8143 apsym 8144 apcotr 8145 apadd1 8146 apneg 8149 mulext1 8150 apti 8160 recexap 8183 creur 8480 creui 8481 cju 8482 cnref1o 9194 replim 10354 cjap 10401 |
Copyright terms: Public domain | W3C validator |