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

Theorem elimel 4555
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 2825 . 2 (𝐴 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐴𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
2 eleq1 2825 . 2 (𝐵 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐵𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
3 elimel.1 . 2 𝐵𝐶
41, 2, 3elimhyp 4551 1 if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  ifcif 4486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-if 4487
This theorem is referenced by:  fprg  7101  orduninsuc  7779  oawordeu  8502  oeoa  8544  omopth  8608  unfilem3  9256  inar1  10711  supsr  11048  renegcl  11464  peano5uzti  12593  eluzaddOLD  12798  eluzsubOLD  12799  ltweuz  13866  uzenom  13869  seqfn  13918  seq1  13919  seqp1  13921  sqeqor  14120  binom2  14121  nn0opth2  14172  faclbnd4lem2  14194  hashxp  14334  dvdsle  16192  divalglem7  16281  divalg  16285  gcdaddm  16405  smadiadetr  22024  iblcnlem  25153  ax5seglem8  27885  elimnv  29625  elimnvu  29626  nmlno0i  29736  nmblolbi  29742  blocn  29749  elimphu  29763  ubth  29815  htth  29860  ifhvhv0  29964  normlem6  30057  norm-iii  30082  norm3lemt  30094  ifchhv  30186  hhssablo  30205  hhssnvt  30207  shscl  30260  shslej  30322  shincl  30323  omlsii  30345  pjoml  30378  pjoc2  30381  chm0  30433  chne0  30436  chocin  30437  chj0  30439  chlejb1  30454  chnle  30456  ledi  30482  h1datom  30524  cmbr3  30550  pjoml2  30553  cmcm  30556  cmcm3  30557  lecm  30559  pjmuli  30631  pjige0  30633  pjhfo  30648  pj11  30656  eigre  30777  eigorth  30780  hoddi  30932  nmlnop0  30940  lnopeq  30951  lnopunilem2  30953  nmbdoplb  30967  nmcopex  30971  nmcoplb  30972  lnopcon  30977  lnfn0  30989  lnfnmul  30990  nmcfnex  30995  nmcfnlb  30996  lnfncon  30998  riesz4  31006  riesz1  31007  cnlnadjeu  31020  pjhmop  31092  pjidmco  31123  mdslmd1lem3  31269  mdslmd1lem4  31270  csmdsymi  31276  hatomic  31302  atord  31330  atcvat2  31331  bnj941  33384  bnj944  33550  kur14  33810  abs2sqle  34268  abs2sqlt  34269  onsucconn  34910  onsucsuccmp  34916  sdclem1  36202  mnurnd  42553  bnd2d  47116
  Copyright terms: Public domain W3C validator