Theorem elimel 3991

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

Syntax hints:   e. wcel 1823   ifcif 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3930

This theorem is referenced by:  fprg  6056  orduninsuc  6651  oawordeu  7196  oeoa  7238  omopth  7299  unfilem3  7778  inar1  9142  supsr  9478  renegcl  9873  peano5uzti  10948  eluzadd  11110  eluzsub  11111  ltweuz  12054  uzenom  12057  seqfn  12101  seq1  12102  seqp1  12104  sqeqor  12264  binom2  12265  nn0opth2  12334  faclbnd4lem2  12354  hashxp  12476  dvdsle  14115  divalglem7  14141  divalg  14145  gcdaddm  14251  smadiadetr  19344  iblcnlem  22361  ax5seglem8  24441  elimnv  25787  elimnvu  25788  nmlno0i  25907  nmblolbi  25913  blocn  25920  elimphu  25934  ubth  25987  htth  26033  ifhvhv0  26137  normlem6  26230  norm-iii  26255  norm3lemt  26267  ifchhv  26360  hhssablo  26377  hhssnvt  26379  shscl  26434  shslej  26496  shincl  26497  omlsii  26519  pjoml  26552  pjoc2  26555  chm0  26607  chne0  26610  chocin  26611  chj0  26613  chlejb1  26628  chnle  26630  ledi  26656  h1datom  26698  cmbr3  26724  pjoml2  26727  cmcm  26730  cmcm3  26731  lecm  26733  pjmuli  26805  pjige0  26807  pjhfo  26822  pj11  26830  eigre  26952  eigorth  26955  hoddi  27107  nmlnop0  27115  lnopeq  27126  lnopunilem2  27128  nmbdoplb  27142  nmcopex  27146  nmcoplb  27147  lnopcon  27152  lnfn0  27164  lnfnmul  27165  nmcfnex  27170  nmcfnlb  27171  lnfncon  27173  riesz4  27181  riesz1  27182  cnlnadjeu  27195  pjhmop  27267  pjidmco  27298  mdslmd1lem3  27444  mdslmd1lem4  27445  csmdsymi  27451  hatomic  27477  atord  27505  atcvat2  27506  kur14  28924  abs2sqle  29310  abs2sqlt  29311  onsuccon  30131  onsucsuccmp  30137  sdclem1  30476  bnj941  34232  bnj944  34397