Theorem elimel 3955

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

Syntax hints:   e. wcel 1758   ifcif 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-if 3895

This theorem is referenced by:  fprg  5995  orduninsuc  6559  oawordeu  7099  oeoa  7141  omopth  7202  unfilem3  7684  inar1  9048  supsr  9385  renegcl  9778  peano5uzti  10837  eluzadd  10995  eluzsub  10996  ltweuz  11896  uzenom  11899  seqfn  11930  seq1  11931  seqp1  11933  sqeqor  12092  binom2  12093  nn0opth2  12162  faclbnd4lem2  12182  hashxp  12309  dvdsle  13691  divalglem7  13716  divalg  13720  gcdaddm  13826  smadiadetr  18608  iblcnlem  21394  ax5seglem8  23329  elimnv  24221  elimnvu  24222  nmlno0i  24341  nmblolbi  24347  blocn  24354  elimphu  24368  ubth  24421  htth  24467  ifhvhv0  24571  normlem6  24664  norm-iii  24689  norm3lemt  24701  ifchhv  24794  hhssablo  24811  hhssnvt  24813  shscl  24868  shslej  24930  shincl  24931  omlsii  24953  pjoml  24986  pjoc2  24989  chm0  25041  chne0  25044  chocin  25045  chj0  25047  chlejb1  25062  chnle  25064  ledi  25090  h1datom  25132  cmbr3  25158  pjoml2  25161  cmcm  25164  cmcm3  25165  lecm  25167  pjmuli  25239  pjige0  25241  pjhfo  25256  pj11  25264  eigre  25386  eigorth  25389  hoddi  25541  nmlnop0  25549  lnopeq  25560  lnopunilem2  25562  nmbdoplb  25576  nmcopex  25580  nmcoplb  25581  lnopcon  25586  lnfn0  25598  lnfnmul  25599  nmcfnex  25604  nmcfnlb  25605  lnfncon  25607  riesz4  25615  riesz1  25616  cnlnadjeu  25629  pjhmop  25701  pjidmco  25732  mdslmd1lem3  25878  mdslmd1lem4  25879  csmdsymi  25885  hatomic  25911  atord  25939  atcvat2  25940  kur14  27243  abs2sqle  27464  abs2sqlt  27465  onsuccon  28423  onsucsuccmp  28429  sdclem1  28782  bnj941  32079  bnj944  32244