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

Theorem elimel 4183
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 2718 . 2 (𝐴 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐴𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
2 eleq1 2718 . 2 (𝐵 = if(𝐴𝐶, 𝐴, 𝐵) → (𝐵𝐶 ↔ if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶))
3 elimel.1 . 2 𝐵𝐶
41, 2, 3elimhyp 4179 1 if(𝐴𝐶, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120
This theorem is referenced by:  fprg  6462  orduninsuc  7085  oawordeu  7680  oeoa  7722  omopth  7783  unfilem3  8267  inar1  9635  supsr  9971  renegcl  10382  peano5uzti  11505  eluzadd  11754  eluzsub  11755  ltweuz  12800  uzenom  12803  seqfn  12853  seq1  12854  seqp1  12856  sqeqor  13018  binom2  13019  nn0opth2  13099  faclbnd4lem2  13121  hashxp  13259  dvdsle  15079  divalglem7  15169  divalg  15173  gcdaddm  15293  smadiadetr  20529  iblcnlem  23600  ax5seglem8  25861  elimnv  27666  elimnvu  27667  nmlno0i  27777  nmblolbi  27783  blocn  27790  elimphu  27804  ubth  27857  htth  27903  ifhvhv0  28007  normlem6  28100  norm-iii  28125  norm3lemt  28137  ifchhv  28229  hhssablo  28248  hhssnvt  28250  shscl  28305  shslej  28367  shincl  28368  omlsii  28390  pjoml  28423  pjoc2  28426  chm0  28478  chne0  28481  chocin  28482  chj0  28484  chlejb1  28499  chnle  28501  ledi  28527  h1datom  28569  cmbr3  28595  pjoml2  28598  cmcm  28601  cmcm3  28602  lecm  28604  pjmuli  28676  pjige0  28678  pjhfo  28693  pj11  28701  eigre  28822  eigorth  28825  hoddi  28977  nmlnop0  28985  lnopeq  28996  lnopunilem2  28998  nmbdoplb  29012  nmcopex  29016  nmcoplb  29017  lnopcon  29022  lnfn0  29034  lnfnmul  29035  nmcfnex  29040  nmcfnlb  29041  lnfncon  29043  riesz4  29051  riesz1  29052  cnlnadjeu  29065  pjhmop  29137  pjidmco  29168  mdslmd1lem3  29314  mdslmd1lem4  29315  csmdsymi  29321  hatomic  29347  atord  29375  atcvat2  29376  bnj941  30969  bnj944  31134  kur14  31324  abs2sqle  31700  abs2sqlt  31701  onsucconn  32562  onsucsuccmp  32568  sdclem1  33669  bnd2d  42753
  Copyright terms: Public domain W3C validator