MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elimel Unicode version

Theorem elimel 4004
Description: Eliminate a membership hypothesis for weak deduction theorem, when special case is provable. (Contributed by NM, 15-May-1999.)
Hypothesis
Ref Expression
elimel.1
Assertion
Ref Expression
elimel

Proof of Theorem elimel
StepHypRef Expression
1 eleq1 2529 . 2
2 eleq1 2529 . 2
3 elimel.1 . 2
41, 2, 3elimhyp 4000 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  ifcif 3941
This theorem is referenced by:  fprg  6080  orduninsuc  6678  oawordeu  7223  oeoa  7265  omopth  7326  unfilem3  7806  inar1  9174  supsr  9510  renegcl  9905  peano5uzti  10977  eluzadd  11138  eluzsub  11139  ltweuz  12072  uzenom  12075  seqfn  12119  seq1  12120  seqp1  12122  sqeqor  12282  binom2  12283  nn0opth2  12352  faclbnd4lem2  12372  hashxp  12492  dvdsle  14031  divalglem7  14057  divalg  14061  gcdaddm  14167  smadiadetr  19177  iblcnlem  22195  ax5seglem8  24239  elimnv  25589  elimnvu  25590  nmlno0i  25709  nmblolbi  25715  blocn  25722  elimphu  25736  ubth  25789  htth  25835  ifhvhv0  25939  normlem6  26032  norm-iii  26057  norm3lemt  26069  ifchhv  26162  hhssablo  26179  hhssnvt  26181  shscl  26236  shslej  26298  shincl  26299  omlsii  26321  pjoml  26354  pjoc2  26357  chm0  26409  chne0  26412  chocin  26413  chj0  26415  chlejb1  26430  chnle  26432  ledi  26458  h1datom  26500  cmbr3  26526  pjoml2  26529  cmcm  26532  cmcm3  26533  lecm  26535  pjmuli  26607  pjige0  26609  pjhfo  26624  pj11  26632  eigre  26754  eigorth  26757  hoddi  26909  nmlnop0  26917  lnopeq  26928  lnopunilem2  26930  nmbdoplb  26944  nmcopex  26948  nmcoplb  26949  lnopcon  26954  lnfn0  26966  lnfnmul  26967  nmcfnex  26972  nmcfnlb  26973  lnfncon  26975  riesz4  26983  riesz1  26984  cnlnadjeu  26997  pjhmop  27069  pjidmco  27100  mdslmd1lem3  27246  mdslmd1lem4  27247  csmdsymi  27253  hatomic  27279  atord  27307  atcvat2  27308  kur14  28660  abs2sqle  29046  abs2sqlt  29047  onsuccon  29903  onsucsuccmp  29909  sdclem1  30236  bnj941  33831  bnj944  33996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942
  Copyright terms: Public domain W3C validator