Theorem elimel 4002

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

Syntax hints:   e. wcel 1767   ifcif 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940

This theorem is referenced by:  fprg  6068  orduninsuc  6656  oawordeu  7201  oeoa  7243  omopth  7304  unfilem3  7782  inar1  9149  supsr  9485  renegcl  9878  peano5uzti  10946  eluzadd  11106  eluzsub  11107  ltweuz  12036  uzenom  12039  seqfn  12083  seq1  12084  seqp1  12086  sqeqor  12246  binom2  12247  nn0opth2  12316  faclbnd4lem2  12336  hashxp  12454  dvdsle  13886  divalglem7  13912  divalg  13916  gcdaddm  14022  smadiadetr  18944  iblcnlem  21930  ax5seglem8  23915  elimnv  25265  elimnvu  25266  nmlno0i  25385  nmblolbi  25391  blocn  25398  elimphu  25412  ubth  25465  htth  25511  ifhvhv0  25615  normlem6  25708  norm-iii  25733  norm3lemt  25745  ifchhv  25838  hhssablo  25855  hhssnvt  25857  shscl  25912  shslej  25974  shincl  25975  omlsii  25997  pjoml  26030  pjoc2  26033  chm0  26085  chne0  26088  chocin  26089  chj0  26091  chlejb1  26106  chnle  26108  ledi  26134  h1datom  26176  cmbr3  26202  pjoml2  26205  cmcm  26208  cmcm3  26209  lecm  26211  pjmuli  26283  pjige0  26285  pjhfo  26300  pj11  26308  eigre  26430  eigorth  26433  hoddi  26585  nmlnop0  26593  lnopeq  26604  lnopunilem2  26606  nmbdoplb  26620  nmcopex  26624  nmcoplb  26625  lnopcon  26630  lnfn0  26642  lnfnmul  26643  nmcfnex  26648  nmcfnlb  26649  lnfncon  26651  riesz4  26659  riesz1  26660  cnlnadjeu  26673  pjhmop  26745  pjidmco  26776  mdslmd1lem3  26922  mdslmd1lem4  26923  csmdsymi  26929  hatomic  26955  atord  26983  atcvat2  26984  kur14  28300  abs2sqle  28521  abs2sqlt  28522  onsuccon  29480  onsucsuccmp  29486  sdclem1  29839  bnj941  32910  bnj944  33075