![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleqtrdi | Unicode version |
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
eleqtrdi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eleqtrdi.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eleqtrdi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleqtrdi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eleqtrdi.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | eleqtrd 2219 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 |
This theorem is referenced by: eleqtrrdi 2234 prid2g 3636 freccllem 6307 finomni 7020 exmidomniim 7021 ismkvnex 7037 exmidaclem 7081 caucvgprprlem2 7542 gt0srpr 7580 eluzel2 9355 fseq1p1m1 9905 fznn0sub2 9936 nn0split 9944 nnsplit 9945 exple1 10380 bcval5 10541 bcpasc 10544 zfz1isolemsplit 10613 seq3coll 10617 clim2ser 11138 clim2ser2 11139 iserex 11140 isermulc2 11141 iserle 11143 iserge0 11144 climub 11145 climserle 11146 serf0 11153 summodclem3 11181 summodclem2a 11182 fsum3 11188 sum0 11189 fsumcl2lem 11199 fsumadd 11207 isumclim3 11224 isumadd 11232 fsump1i 11234 fsummulc2 11249 cvgcmpub 11277 binom1dif 11288 isumshft 11291 isumsplit 11292 isumrpcl 11295 arisum2 11300 trireciplem 11301 geoserap 11308 geolim 11312 geo2lim 11317 cvgratnnlemnexp 11325 cvgratnnlemseq 11327 cvgratgt0 11334 mertenslemi1 11336 mertenslem2 11337 mertensabs 11338 clim2prod 11340 clim2divap 11341 prodmodclem3 11376 prodmodclem2a 11377 fprodseq 11384 efcvgfsum 11410 efcj 11416 effsumlt 11435 mod2eq1n2dvds 11612 algrp1 11763 phiprmpw 11934 crth 11936 phimullem 11937 ennnfonelemp1 11955 istps 12238 topontopn 12243 cldrcl 12310 cnrehmeocntop 12801 nnsf 13374 nninfsellemqall 13386 nninfomnilem 13389 cvgcmp2nlemabs 13402 trilpolemeq1 13408 |
Copyright terms: Public domain | W3C validator |