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 7518 gt0srpr 7556 eluzel2 9331 fseq1p1m1 9874 fznn0sub2 9905 nn0split 9913 nnsplit 9914 exple1 10349 bcval5 10509 bcpasc 10512 zfz1isolemsplit 10581 seq3coll 10585 clim2ser 11106 clim2ser2 11107 iserex 11108 isermulc2 11109 iserle 11111 iserge0 11112 climub 11113 climserle 11114 serf0 11121 summodclem3 11149 summodclem2a 11150 fsum3 11156 sum0 11157 fsumcl2lem 11167 fsumadd 11175 isumclim3 11192 isumadd 11200 fsump1i 11202 fsummulc2 11217 cvgcmpub 11245 binom1dif 11256 isumshft 11259 isumsplit 11260 isumrpcl 11263 arisum2 11268 trireciplem 11269 geoserap 11276 geolim 11280 geo2lim 11285 cvgratnnlemnexp 11293 cvgratnnlemseq 11295 cvgratgt0 11302 mertenslemi1 11304 mertenslem2 11305 mertensabs 11306 clim2prod 11308 clim2divap 11309 prodmodclem3 11344 prodmodclem2a 11345 efcvgfsum 11373 efcj 11379 effsumlt 11398 mod2eq1n2dvds 11576 algrp1 11727 phiprmpw 11898 crth 11900 phimullem 11901 ennnfonelemp1 11919 istps 12199 topontopn 12204 cldrcl 12271 cnrehmeocntop 12762 nnsf 13199 nninfsellemqall 13211 nninfomnilem 13214 cvgcmp2nlemabs 13227 trilpolemeq1 13233 |
Copyright terms: Public domain | W3C validator |