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 2218 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 wcel 1480 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-clel 2135 |
This theorem is referenced by: eleqtrrdi 2233 prid2g 3628 freccllem 6299 finomni 7012 exmidomniim 7013 ismkvnex 7029 exmidaclem 7064 caucvgprprlem2 7521 gt0srpr 7559 eluzel2 9334 fseq1p1m1 9877 fznn0sub2 9908 nn0split 9916 nnsplit 9917 exple1 10352 bcval5 10512 bcpasc 10515 zfz1isolemsplit 10584 seq3coll 10588 clim2ser 11109 clim2ser2 11110 iserex 11111 isermulc2 11112 iserle 11114 iserge0 11115 climub 11116 climserle 11117 serf0 11124 summodclem3 11152 summodclem2a 11153 fsum3 11159 sum0 11160 fsumcl2lem 11170 fsumadd 11178 isumclim3 11195 isumadd 11203 fsump1i 11205 fsummulc2 11220 cvgcmpub 11248 binom1dif 11259 isumshft 11262 isumsplit 11263 isumrpcl 11266 arisum2 11271 trireciplem 11272 geoserap 11279 geolim 11283 geo2lim 11288 cvgratnnlemnexp 11296 cvgratnnlemseq 11298 cvgratgt0 11305 mertenslemi1 11307 mertenslem2 11308 mertensabs 11309 clim2prod 11311 clim2divap 11312 prodmodclem3 11347 prodmodclem2a 11348 efcvgfsum 11376 efcj 11382 effsumlt 11401 mod2eq1n2dvds 11579 algrp1 11730 phiprmpw 11901 crth 11903 phimullem 11904 ennnfonelemp1 11922 istps 12202 topontopn 12207 cldrcl 12274 cnrehmeocntop 12765 nnsf 13202 nninfsellemqall 13214 nninfomnilem 13217 cvgcmp2nlemabs 13230 trilpolemeq1 13236 |
Copyright terms: Public domain | W3C validator |