![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elequ2 | Unicode version |
Description: An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
elequ2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-14 2151 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-14 2151 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | equcoms 1708 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | impbid 129 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1449 ax-ie2 1494 ax-8 1504 ax-17 1526 ax-i9 1530 ax-14 2151 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: elsb2 2156 dveel2 2158 axext3 2160 axext4 2161 bm1.1 2162 eleq2w 2239 bm1.3ii 4124 nalset 4133 zfun 4434 fv3 5538 tfrlemisucaccv 6325 tfr1onlemsucaccv 6341 tfrcllemsucaccv 6354 acfun 7205 ccfunen 7262 cc1 7263 bdsepnft 14521 bdsepnfALT 14523 bdbm1.3ii 14525 bj-nalset 14529 bj-nnelirr 14587 nninfalllem1 14639 nninfsellemeq 14645 nninfsellemqall 14646 nninfsellemeqinf 14647 nninfomni 14650 |
Copyright terms: Public domain | W3C validator |