MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplbi Unicode version

Theorem simplbi 460
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simplbi.1
Assertion
Ref Expression
simplbi

Proof of Theorem simplbi
StepHypRef Expression
1 simplbi.1 . . 3
21biimpi 194 . 2
32simpld 459 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  3simpa  993  xoror  1370  sbequ2  1741  reurex  3074  eqimss  3555  pssss  3598  eldifi  3625  inss1  3717  ssunsn2  4189  pwssun  4791  sopo  4822  wefr  4874  ordtr  4897  opelxp1  5037  relop  5158  funmo  5609  funrel  5610  fnfun  5683  ffn  5736  f1f  5786  f1of1  5820  f1ofo  5828  isof1o  6221  eqopi  6834  1st2nd2  6837  reldmtpos  6982  swoer  7358  erdisj  7378  ecopover  7434  sdomdom  7563  mapfien  7887  inf3lemd  8065  mapfienOLD  8159  cardprclem  8381  infxpenlem  8412  cardinfima  8499  dfac5lem4  8528  domtriomlem  8843  smobeth  8982  fpwwe2lem6  9034  fpwwe2lem7  9035  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  axrnegex  9560  axpre-sup  9567  zre  10893  nnssz  10909  ixxss1  11576  ixxss2  11577  ixxss12  11578  lbioo  11589  ubioo  11590  iccss2  11624  rge0ssre  11657  elfzuz  11713  uzdisj  11780  nn0disj  11820  0wrd0  12566  splfv1  12731  sqrlem6  13081  rlimf  13324  lo1f  13341  lo1dm  13342  o1f  13352  o1dm  13353  mertenslem2  13694  divalglem9  14059  bitsinv2  14093  bitsf1ocnv  14094  gcdcllem1  14149  prmnn  14220  prmuz2  14235  phimullem  14309  1arith  14445  ramtlecl  14518  0ramcl  14541  firest  14830  acsmre  15049  posprs  15578  latpos  15680  clatpos  15740  dlatl  15825  pslem  15836  tsrlemax  15850  tsrps  15851  sgrpmgm  15916  mndsgrp  15927  grpmnd  16062  nsgsubg  16233  ghmgrp1  16269  ghmgrp2  16270  gimghm  16312  gagrp  16330  gaset  16331  psgneu  16531  efgredeu  16770  ablgrp  16803  cmnmnd  16813  cyggenod2  16888  cyggrp  16892  ablfac2  17140  crngring  17209  dvdsrcl  17298  unitcl  17308  brric2  17394  drngring  17403  subrgring  17432  subrgrcl  17434  srngrhm  17500  lmimlmhm  17710  lveclmod  17752  2idlcpbl  17882  qus1  17883  qusrhm  17885  lpirring  17900  nzrring  17909  domnnzr  17944  fldidom  17954  assalmod  17968  assaring  17969  assasca  17970  cygznlem1  18605  cygznlem3  18608  lbslinds  18868  gsummatr01lem1  19157  topontop  19427  tpstop  19440  clsval2  19551  mretopd  19593  neiptoptop  19632  perftop  19657  restfpw  19680  cntop1  19741  cntop2  19742  cnptop1  19743  cnptop2  19744  cnprcl  19746  t1ficld  19828  t0top  19830  t1top  19831  haustop  19832  regtop  19834  nrmtop  19837  cnrmtop  19838  pnrmnrm  19841  cmptop  19895  discmp  19898  tgcmp  19901  uncmp  19903  conndisj  19917  contop  19918  1stctop  19944  llytop  19973  nllytop  19974  hmeocn  20261  filfbas  20349  ufilfil  20405  flimtop  20466  flimfil  20470  alexsublem  20544  ptcmplem3  20554  tsmsfbas  20626  tsmslem1  20627  tsmsgsum  20637  tsmsgsumOLD  20640  tsmssubm  20644  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  tsmsmhm  20648  tsmsadd  20649  tsmsxplem1  20655  tsmsxplem2  20656  tsmsxp  20657  tlmtmd  20689  tlmlmod  20691  tlmtrg  20692  tvctlm  20699  ressust  20767  uspreg  20777  ucncn  20788  neipcfilu  20799  cuspusp  20803  isxmet2d  20830  metxmet  20837  xmstps  20956  msxms  20957  xmsxmet  20959  msmet  20960  stdbdxmet  21018  nrgngp  21171  nlmngp  21186  nlmlmod  21187  nlmnrg  21188  nvcnlm  21204  nmoi  21235  nghmrcl1  21239  nghmrcl2  21240  nmhmrcl1  21254  nmhmrcl2  21255  qdensere  21277  xrge0gsumle  21338  xrge0tsms  21339  metds0  21354  metdstri  21355  metdsre  21357  metdseq0  21358  metdscnlem  21359  metnrmlem1a  21362  metnrmlem1  21363  icopnfcnv  21442  cvsclm  21607  cmetmet  21725  cmsms  21787  hlbn  21803  ovolicc2lem5  21932  mblss  21942  mbff  22034  mbfres  22051  mbfadd  22068  mbfsub  22069  i1fmbf  22082  mbfmul  22133  bddmulibl  22245  limcmpt  22287  c1liplem1  22397  c1lip2  22399  fta1glem1  22566  fta1glem2  22567  fta1g  22568  fta1b  22570  ply1pid  22580  aacn  22713  ulmf2  22779  logdmnrp  23022  logdmss  23023  logcnlem2  23024  logcnlem3  23025  logcnlem4  23026  logcnlem5  23027  logcn  23028  dvloglem  23029  logf1o2  23031  efopnlem1  23037  logtayl2  23043  cxpcn  23119  cxpcn3lem  23121  cxpcn3  23122  resqrtcn  23123  atandmneg  23237  atandmcj  23240  cosatan  23252  cosatanne0  23253  birthdaylem1  23281  areacl  23292  cxp2lim  23306  jensenlem2  23317  jensen  23318  sqff1o  23456  dvdsmulf1o  23470  lgsqrlem1  23616  lgsqrlem2  23617  lgsqrlem3  23618  lgsqrlem4  23619  lgseisenlem3  23626  chebbnd1  23657  chtppilim  23660  chpchtlim  23664  chpo1ub  23665  dchrmusumlema  23678  dchrvmasumiflem1  23686  dchrisum0lema  23699  dchrisum0lem2  23703  selberg3lem2  23743  pntrsumo1  23750  selbergsb  23760  pnt2  23798  tglineeltr  24011  axcontlem2  24268  axcontlem7  24273  axcontlem8  24274  uhgra0v  24310  usgra0v  24371  usgra1v  24390  eupagra  24966  frgrawopreg  25049  ablogrpo  25286  smgrpismgmOLD  25334  mndoissmgrpOLD  25341  bnnv  25782  hlobn  25804  hcauseq  26102  hlimseqi  26106  hlimveci  26107  shss  26127  sh0  26133  chsh  26142  lnopf  26778  bdopln  26780  hmopf  26793  lnfnf  26803  unopf1o  26835  elunop2  26932  elpjhmop  27104  stcltrlem1  27195  mdslle1i  27236  mdslle2i  27237  rabexgfGS  27401  ssnnssfz  27597  tospos  27646  ogrpgrp  27693  ogrpinvOLD  27705  xrge0tsmsd  27775  ofldfld  27800  ofldlt1  27803  ofldchr  27804  isarchiofld  27807  reofld  27830  rearchi  27832  creftop  27849  lmxrge0  27934  qqhrhm  27970  esumpcvgval  28084  measssd  28186  elmbfmvol2  28238  sibfinima  28281  eulerpartlemr  28313  eulerpartlemgf  28318  fiblem  28337  domprobmeas  28349  ballotlemscr  28457  ballotlemfg  28464  ballotlemfrc  28465  ballotlemfrceq  28467  ballotlemrinv0  28471  pcontop  28670  sconpcon  28672  cvmcn  28707  cvmliftlem10  28739  fundmpss  29196  predel  29263  sltres  29424  funpartfun  29593  outsideofcol  29783  itg2addnc  30069  fnebas  30162  filnetlem3  30198  istotbnd3  30267  totbndmet  30268  sstotbnd2  30270  sstotbnd  30271  equivtotbnd  30274  bndmet  30277  totbndbnd  30285  prdstotbnd  30290  crngorngo  30397  prrngorngo  30448  divrngpr  30450  an3  30591  nacsacs  30641  eldiophelnn0  30697  lnmlmod  31025  lnrring  31061  mncply  31086  idomrootle  31152  idomodle  31153  hashgcdlem  31157  areaquad  31184  nznngen  31221  binomcxplemcvg  31259  elinel1  31424  fprodge0  31597  stoweidlem14  31796  stoweidlem16  31798  stoweidlem24  31806  stoweidlem51  31833  stoweidlem54  31836  etransclem32  32049  ndmafv  32225  uhg0v  32377  rnghmsubcsetclem1  32783  funcrngcsetcALT  32807  rhmsubcsetclem1  32829  rhmsubcrngclem1  32835  ssnn0ssfz  32938  2uasbanh  33334  bnj563  33800  bnj658  33808  bnj667  33809  bnj570  33963  bnj938  33995  bnj1001  34016  bnj1006  34017  bnj1049  34030  bnj1121  34041  bnj1173  34058  bnj1177  34062  bnj1245  34070  bnj1311  34080  bnj1321  34083  bnj1388  34089  bnj1398  34090  bnj1415  34094  bnj1417  34097  bnj1421  34098  bnj1442  34105  bnj1452  34108  bnj1489  34112  bnj1312  34114  ollat  34938  omlol  34965  cvlatl  35050  hlomcmcv  35081  2dim  35194  1dimN  35195  lcfl8b  37231  lclkrlem2  37259  lclkrslem1  37264  lclkrslem2  37265  lcfrlem9  37277  mapdval2N  37357  mapdordlem2  37364  mapdrvallem2  37372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator