Theorem elimel 3849

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

Syntax hints:   e. wcel 1761   ifcif 3788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-if 3789

This theorem is referenced by:  fprg  5888  orduninsuc  6453  oawordeu  6990  oeoa  7032  omopth  7093  unfilem3  7574  inar1  8938  supsr  9275  renegcl  9668  peano5uzti  10727  eluzadd  10885  eluzsub  10886  ltweuz  11780  uzenom  11783  seqfn  11814  seq1  11815  seqp1  11817  sqeqor  11976  binom2  11977  nn0opth2  12046  faclbnd4lem2  12066  hashxp  12192  dvdsle  13574  divalglem7  13599  divalg  13603  gcdaddm  13709  smadiadetr  18440  iblcnlem  21225  ax5seglem8  23117  elimnv  24009  elimnvu  24010  nmlno0i  24129  nmblolbi  24135  blocn  24142  elimphu  24156  ubth  24209  htth  24255  ifhvhv0  24359  normlem6  24452  norm-iii  24477  norm3lemt  24489  ifchhv  24582  hhssablo  24599  hhssnvt  24601  shscl  24656  shslej  24718  shincl  24719  omlsii  24741  pjoml  24774  pjoc2  24777  chm0  24829  chne0  24832  chocin  24833  chj0  24835  chlejb1  24850  chnle  24852  ledi  24878  h1datom  24920  cmbr3  24946  pjoml2  24949  cmcm  24952  cmcm3  24953  lecm  24955  pjmuli  25027  pjige0  25029  pjhfo  25044  pj11  25052  eigre  25174  eigorth  25177  hoddi  25329  nmlnop0  25337  lnopeq  25348  lnopunilem2  25350  nmbdoplb  25364  nmcopex  25368  nmcoplb  25369  lnopcon  25374  lnfn0  25386  lnfnmul  25387  nmcfnex  25392  nmcfnlb  25393  lnfncon  25395  riesz4  25403  riesz1  25404  cnlnadjeu  25417  pjhmop  25489  pjidmco  25520  mdslmd1lem3  25666  mdslmd1lem4  25667  csmdsymi  25673  hatomic  25699  atord  25727  atcvat2  25728  kur14  27034  abs2sqle  27254  abs2sqlt  27255  onsuccon  28214  onsucsuccmp  28220  sdclem1  28564  bnj941  31600  bnj944  31765