![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > elimel | Structured 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 2524 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eleq1 2524 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | elimel.1 |
. 2
![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | elimhyp 3951 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2438 df-cleq 2444 df-clel 2447 df-if 3895 |
This theorem is referenced by: fprg 5995 orduninsuc 6559 oawordeu 7099 oeoa 7141 omopth 7202 unfilem3 7684 inar1 9048 supsr 9385 renegcl 9778 peano5uzti 10837 eluzadd 10995 eluzsub 10996 ltweuz 11896 uzenom 11899 seqfn 11930 seq1 11931 seqp1 11933 sqeqor 12092 binom2 12093 nn0opth2 12162 faclbnd4lem2 12182 hashxp 12309 dvdsle 13691 divalglem7 13716 divalg 13720 gcdaddm 13826 smadiadetr 18608 iblcnlem 21394 ax5seglem8 23329 elimnv 24221 elimnvu 24222 nmlno0i 24341 nmblolbi 24347 blocn 24354 elimphu 24368 ubth 24421 htth 24467 ifhvhv0 24571 normlem6 24664 norm-iii 24689 norm3lemt 24701 ifchhv 24794 hhssablo 24811 hhssnvt 24813 shscl 24868 shslej 24930 shincl 24931 omlsii 24953 pjoml 24986 pjoc2 24989 chm0 25041 chne0 25044 chocin 25045 chj0 25047 chlejb1 25062 chnle 25064 ledi 25090 h1datom 25132 cmbr3 25158 pjoml2 25161 cmcm 25164 cmcm3 25165 lecm 25167 pjmuli 25239 pjige0 25241 pjhfo 25256 pj11 25264 eigre 25386 eigorth 25389 hoddi 25541 nmlnop0 25549 lnopeq 25560 lnopunilem2 25562 nmbdoplb 25576 nmcopex 25580 nmcoplb 25581 lnopcon 25586 lnfn0 25598 lnfnmul 25599 nmcfnex 25604 nmcfnlb 25605 lnfncon 25607 riesz4 25615 riesz1 25616 cnlnadjeu 25629 pjhmop 25701 pjidmco 25732 mdslmd1lem3 25878 mdslmd1lem4 25879 csmdsymi 25885 hatomic 25911 atord 25939 atcvat2 25940 kur14 27243 abs2sqle 27464 abs2sqlt 27465 onsuccon 28423 onsucsuccmp 28429 sdclem1 28782 bnj941 32079 bnj944 32244 |
Copyright terms: Public domain | W3C validator |