![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elimel | Structured version Visualization version Unicode version |
Description: Eliminate a membership
hypothesis for weak deduction theorem, when
special case ![]() ![]() ![]() |
Ref | Expression |
---|---|
elimel.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elimel |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2517 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eleq1 2517 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | elimel.1 |
. 2
![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | elimhyp 3939 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-if 3882 |
This theorem is referenced by: fprg 6073 orduninsuc 6670 oawordeu 7256 oeoa 7298 omopth 7359 unfilem3 7837 inar1 9200 supsr 9536 renegcl 9937 peano5uzti 11025 eluzadd 11187 eluzsub 11188 ltweuz 12175 uzenom 12178 seqfn 12225 seq1 12226 seqp1 12228 sqeqor 12388 binom2 12389 nn0opth2 12458 faclbnd4lem2 12479 hashxp 12606 dvdsle 14350 divalglem7 14379 divalg 14384 gcdaddm 14493 smadiadetr 19700 iblcnlem 22746 ax5seglem8 24966 elimnv 26315 elimnvu 26316 nmlno0i 26435 nmblolbi 26441 blocn 26448 elimphu 26462 ubth 26515 htth 26571 ifhvhv0 26675 normlem6 26768 norm-iii 26793 norm3lemt 26805 ifchhv 26897 hhssablo 26914 hhssnvt 26916 shscl 26971 shslej 27033 shincl 27034 omlsii 27056 pjoml 27089 pjoc2 27092 chm0 27144 chne0 27147 chocin 27148 chj0 27150 chlejb1 27165 chnle 27167 ledi 27193 h1datom 27235 cmbr3 27261 pjoml2 27264 cmcm 27267 cmcm3 27268 lecm 27270 pjmuli 27342 pjige0 27344 pjhfo 27359 pj11 27367 eigre 27488 eigorth 27491 hoddi 27643 nmlnop0 27651 lnopeq 27662 lnopunilem2 27664 nmbdoplb 27678 nmcopex 27682 nmcoplb 27683 lnopcon 27688 lnfn0 27700 lnfnmul 27701 nmcfnex 27706 nmcfnlb 27707 lnfncon 27709 riesz4 27717 riesz1 27718 cnlnadjeu 27731 pjhmop 27803 pjidmco 27834 mdslmd1lem3 27980 mdslmd1lem4 27981 csmdsymi 27987 hatomic 28013 atord 28041 atcvat2 28042 bnj941 29584 bnj944 29749 kur14 29939 abs2sqle 30324 abs2sqlt 30325 onsuccon 31098 onsucsuccmp 31104 sdclem1 32072 |
Copyright terms: Public domain | W3C validator |