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

Theorem elimel 4529
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 if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶

Proof of Theorem elimel
StepHypRef Expression
1 eleq1 2827 . 2 (𝐴 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐴𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
2 eleq1 2827 . 2 (𝐵 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐵𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
3 elimel.1 . 2 𝐵𝐶
41, 2, 3elimhyp 4525 1 if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  ifcif 4460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4461
This theorem is referenced by:  fprg  7036  orduninsuc  7699  oawordeu  8395  oeoa  8437  omopth  8501  unfilem3  9089  inar1  10540  supsr  10877  renegcl  11293  peano5uzti  12419  eluzadd  12622  eluzsub  12623  ltweuz  13690  uzenom  13693  seqfn  13742  seq1  13743  seqp1  13745  sqeqor  13941  binom2  13942  nn0opth2  13995  faclbnd4lem2  14017  hashxp  14158  dvdsle  16028  divalglem7  16117  divalg  16121  gcdaddm  16241  smadiadetr  21833  iblcnlem  24962  ax5seglem8  27313  elimnv  29054  elimnvu  29055  nmlno0i  29165  nmblolbi  29171  blocn  29178  elimphu  29192  ubth  29244  htth  29289  ifhvhv0  29393  normlem6  29486  norm-iii  29511  norm3lemt  29523  ifchhv  29615  hhssablo  29634  hhssnvt  29636  shscl  29689  shslej  29751  shincl  29752  omlsii  29774  pjoml  29807  pjoc2  29810  chm0  29862  chne0  29865  chocin  29866  chj0  29868  chlejb1  29883  chnle  29885  ledi  29911  h1datom  29953  cmbr3  29979  pjoml2  29982  cmcm  29985  cmcm3  29986  lecm  29988  pjmuli  30060  pjige0  30062  pjhfo  30077  pj11  30085  eigre  30206  eigorth  30209  hoddi  30361  nmlnop0  30369  lnopeq  30380  lnopunilem2  30382  nmbdoplb  30396  nmcopex  30400  nmcoplb  30401  lnopcon  30406  lnfn0  30418  lnfnmul  30419  nmcfnex  30424  nmcfnlb  30425  lnfncon  30427  riesz4  30435  riesz1  30436  cnlnadjeu  30449  pjhmop  30521  pjidmco  30552  mdslmd1lem3  30698  mdslmd1lem4  30699  csmdsymi  30705  hatomic  30731  atord  30759  atcvat2  30760  bnj941  32761  bnj944  32927  kur14  33187  abs2sqle  33647  abs2sqlt  33648  onsucconn  34636  onsucsuccmp  34642  sdclem1  35910  mnurnd  41908  bnd2d  46398
  Copyright terms: Public domain W3C validator