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

Theorem elimel 4537
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 2905 . 2 (𝐴 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐴𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
2 eleq1 2905 . 2 (𝐵 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐵𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
3 elimel.1 . 2 𝐵𝐶
41, 2, 3elimhyp 4533 1 if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  ifcif 4470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-if 4471
This theorem is referenced by:  fprg  6915  orduninsuc  7551  oawordeu  8176  oeoa  8218  omopth  8280  unfilem3  8778  inar1  10191  supsr  10528  renegcl  10943  peano5uzti  12066  eluzadd  12267  eluzsub  12268  ltweuz  13324  uzenom  13327  seqfn  13376  seq1  13377  seqp1  13379  sqeqor  13573  binom2  13574  nn0opth2  13627  faclbnd4lem2  13649  hashxp  13790  dvdsle  15655  divalglem7  15745  divalg  15749  gcdaddm  15868  smadiadetr  21219  iblcnlem  24323  ax5seglem8  26655  elimnv  28393  elimnvu  28394  nmlno0i  28504  nmblolbi  28510  blocn  28517  elimphu  28531  ubth  28583  htth  28628  ifhvhv0  28732  normlem6  28825  norm-iii  28850  norm3lemt  28862  ifchhv  28954  hhssablo  28973  hhssnvt  28975  shscl  29028  shslej  29090  shincl  29091  omlsii  29113  pjoml  29146  pjoc2  29149  chm0  29201  chne0  29204  chocin  29205  chj0  29207  chlejb1  29222  chnle  29224  ledi  29250  h1datom  29292  cmbr3  29318  pjoml2  29321  cmcm  29324  cmcm3  29325  lecm  29327  pjmuli  29399  pjige0  29401  pjhfo  29416  pj11  29424  eigre  29545  eigorth  29548  hoddi  29700  nmlnop0  29708  lnopeq  29719  lnopunilem2  29721  nmbdoplb  29735  nmcopex  29739  nmcoplb  29740  lnopcon  29745  lnfn0  29757  lnfnmul  29758  nmcfnex  29763  nmcfnlb  29764  lnfncon  29766  riesz4  29774  riesz1  29775  cnlnadjeu  29788  pjhmop  29860  pjidmco  29891  mdslmd1lem3  30037  mdslmd1lem4  30038  csmdsymi  30044  hatomic  30070  atord  30098  atcvat2  30099  bnj941  31949  bnj944  32115  kur14  32366  abs2sqle  32826  abs2sqlt  32827  onsucconn  33689  onsucsuccmp  33695  sdclem1  34905  mnurnd  40503  bnd2d  44686
  Copyright terms: Public domain W3C validator