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

Theorem elimel 4559
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 2822 . 2 (𝐴 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐴𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
2 eleq1 2822 . 2 (𝐵 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐵𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
3 elimel.1 . 2 𝐵𝐶
41, 2, 3elimhyp 4555 1 if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  ifcif 4490
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 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4491
This theorem is referenced by:  fprg  7105  orduninsuc  7783  oawordeu  8506  oeoa  8548  omopth  8612  unfilem3  9262  inar1  10719  supsr  11056  renegcl  11472  peano5uzti  12601  eluzaddOLD  12806  eluzsubOLD  12807  ltweuz  13875  uzenom  13878  seqfn  13927  seq1  13928  seqp1  13930  sqeqor  14129  binom2  14130  nn0opth2  14181  faclbnd4lem2  14203  hashxp  14343  dvdsle  16200  divalglem7  16289  divalg  16293  gcdaddm  16413  smadiadetr  22047  iblcnlem  25176  ax5seglem8  27934  elimnv  29674  elimnvu  29675  nmlno0i  29785  nmblolbi  29791  blocn  29798  elimphu  29812  ubth  29864  htth  29909  ifhvhv0  30013  normlem6  30106  norm-iii  30131  norm3lemt  30143  ifchhv  30235  hhssablo  30254  hhssnvt  30256  shscl  30309  shslej  30371  shincl  30372  omlsii  30394  pjoml  30427  pjoc2  30430  chm0  30482  chne0  30485  chocin  30486  chj0  30488  chlejb1  30503  chnle  30505  ledi  30531  h1datom  30573  cmbr3  30599  pjoml2  30602  cmcm  30605  cmcm3  30606  lecm  30608  pjmuli  30680  pjige0  30682  pjhfo  30697  pj11  30705  eigre  30826  eigorth  30829  hoddi  30981  nmlnop0  30989  lnopeq  31000  lnopunilem2  31002  nmbdoplb  31016  nmcopex  31020  nmcoplb  31021  lnopcon  31026  lnfn0  31038  lnfnmul  31039  nmcfnex  31044  nmcfnlb  31045  lnfncon  31047  riesz4  31055  riesz1  31056  cnlnadjeu  31069  pjhmop  31141  pjidmco  31172  mdslmd1lem3  31318  mdslmd1lem4  31319  csmdsymi  31325  hatomic  31351  atord  31379  atcvat2  31380  bnj941  33448  bnj944  33614  kur14  33874  abs2sqle  34332  abs2sqlt  34333  onsucconn  34963  onsucsuccmp  34969  sdclem1  36252  mnurnd  42655  bnd2d  47216
  Copyright terms: Public domain W3C validator