Theorem elimel 3985

Description: Eliminate a membership hypothesis for weak deduction theorem, when special case B e. C is provable. (Contributed by NM, 15-May-1999.)

Hypothesis

Ref	Expression
elimel.1	|- B e. C

Assertion

Ref	Expression
elimel	|- if ( A e. C , A , B ) e. C

Proof of Theorem elimel

Step	Hyp	Ref	Expression
1		eleq1 2513	. 2 |- ( A = if ( A e. C , A , B ) -> ( A e. C <-> if ( A e. C , A , B ) e. C ) )
2		eleq1 2513	. 2 |- ( B = if ( A e. C , A , B ) -> ( B e. C <-> if ( A e. C , A , B ) e. C ) )
3		elimel.1	. 2 |- B e. C
4	1, 2, 3	elimhyp 3981	1 |- if ( A e. C , A , B ) e. C

Syntax hints:   e. wcel 1802   ifcif 3922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-if 3923

This theorem is referenced by:  fprg  6061  orduninsuc  6659  oawordeu  7202  oeoa  7244  omopth  7305  unfilem3  7784  inar1  9151  supsr  9487  renegcl  9882  peano5uzti  10953  eluzadd  11113  eluzsub  11114  ltweuz  12046  uzenom  12049  seqfn  12093  seq1  12094  seqp1  12096  sqeqor  12256  binom2  12257  nn0opth2  12326  faclbnd4lem2  12346  hashxp  12466  dvdsle  13903  divalglem7  13929  divalg  13933  gcdaddm  14039  smadiadetr  19044  iblcnlem  22061  ax5seglem8  24104  elimnv  25454  elimnvu  25455  nmlno0i  25574  nmblolbi  25580  blocn  25587  elimphu  25601  ubth  25654  htth  25700  ifhvhv0  25804  normlem6  25897  norm-iii  25922  norm3lemt  25934  ifchhv  26027  hhssablo  26044  hhssnvt  26046  shscl  26101  shslej  26163  shincl  26164  omlsii  26186  pjoml  26219  pjoc2  26222  chm0  26274  chne0  26277  chocin  26278  chj0  26280  chlejb1  26295  chnle  26297  ledi  26323  h1datom  26365  cmbr3  26391  pjoml2  26394  cmcm  26397  cmcm3  26398  lecm  26400  pjmuli  26472  pjige0  26474  pjhfo  26489  pj11  26497  eigre  26619  eigorth  26622  hoddi  26774  nmlnop0  26782  lnopeq  26793  lnopunilem2  26795  nmbdoplb  26809  nmcopex  26813  nmcoplb  26814  lnopcon  26819  lnfn0  26831  lnfnmul  26832  nmcfnex  26837  nmcfnlb  26838  lnfncon  26840  riesz4  26848  riesz1  26849  cnlnadjeu  26862  pjhmop  26934  pjidmco  26965  mdslmd1lem3  27111  mdslmd1lem4  27112  csmdsymi  27118  hatomic  27144  atord  27172  atcvat2  27173  kur14  28526  abs2sqle  28912  abs2sqlt  28913  onsuccon  29871  onsucsuccmp  29877  sdclem1  30204  bnj941  33538  bnj944  33703