Theorem elimel 3943

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 2517	. 2 |- ( A = if ( A e. C , A , B ) -> ( A e. C <-> if ( A e. C , A , B ) e. C ) )
2		eleq1 2517	. 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 3939	1 |- if ( A e. C , A , B ) e. C

Syntax hints:   e. wcel 1887   ifcif 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-if 3882

This theorem is referenced by:  fprg  6073  orduninsuc  6670  oawordeu  7256  oeoa  7298  omopth  7359  unfilem3  7837  inar1  9200  supsr  9536  renegcl  9937  peano5uzti  11025  eluzadd  11187  eluzsub  11188  ltweuz  12175  uzenom  12178  seqfn  12225  seq1  12226  seqp1  12228  sqeqor  12388  binom2  12389  nn0opth2  12458  faclbnd4lem2  12479  hashxp  12606  dvdsle  14350  divalglem7  14379  divalg  14384  gcdaddm  14493  smadiadetr  19700  iblcnlem  22746  ax5seglem8  24966  elimnv  26315  elimnvu  26316  nmlno0i  26435  nmblolbi  26441  blocn  26448  elimphu  26462  ubth  26515  htth  26571  ifhvhv0  26675  normlem6  26768  norm-iii  26793  norm3lemt  26805  ifchhv  26897  hhssablo  26914  hhssnvt  26916  shscl  26971  shslej  27033  shincl  27034  omlsii  27056  pjoml  27089  pjoc2  27092  chm0  27144  chne0  27147  chocin  27148  chj0  27150  chlejb1  27165  chnle  27167  ledi  27193  h1datom  27235  cmbr3  27261  pjoml2  27264  cmcm  27267  cmcm3  27268  lecm  27270  pjmuli  27342  pjige0  27344  pjhfo  27359  pj11  27367  eigre  27488  eigorth  27491  hoddi  27643  nmlnop0  27651  lnopeq  27662  lnopunilem2  27664  nmbdoplb  27678  nmcopex  27682  nmcoplb  27683  lnopcon  27688  lnfn0  27700  lnfnmul  27701  nmcfnex  27706  nmcfnlb  27707  lnfncon  27709  riesz4  27717  riesz1  27718  cnlnadjeu  27731  pjhmop  27803  pjidmco  27834  mdslmd1lem3  27980  mdslmd1lem4  27981  csmdsymi  27987  hatomic  28013  atord  28041  atcvat2  28042  bnj941  29584  bnj944  29749  kur14  29939  abs2sqle  30324  abs2sqlt  30325  onsuccon  31098  onsucsuccmp  31104  sdclem1  32072