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

Theorem simplbi 450
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 188 . 2
32simpld 449 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  /\wa 362
This theorem is referenced by:  3simpa  970  xoror  1342  sbequ2  1695  reurex  2916  eqimss  3385  pssss  3428  eldifi  3455  inss1  3547  ssunsn2  4007  pwssun  4598  sopo  4629  wefr  4681  ordtr  4704  opelxp1  4843  relop  4961  xpdifid  5238  funmo  5406  funrel  5407  fnfun  5478  ffn  5529  f1f  5576  f1of1  5610  f1ofo  5618  isof1o  5984  eqopi  6579  1st2nd2  6582  reldmtpos  6715  swoer  7090  erdisj  7109  ecopover  7165  sdomdom  7296  mapfien  7604  inf3lemd  7780  mapfienOLD  7874  cardprclem  8096  infxpenlem  8127  cardinfima  8214  dfac5lem4  8243  domtriomlem  8558  smobeth  8697  fpwwe2lem6  8748  fpwwe2lem7  8749  fpwwe2lem12  8754  fpwwe2lem13  8755  fpwwe2  8756  axrnegex  9275  axpre-sup  9282  zre  10595  nnssz  10611  ixxss1  11263  ixxss2  11264  ixxss12  11265  lbioo  11276  ubioo  11277  iccss2  11311  elfzuz  11393  uzdisj  11472  0wrd0  12194  splfv1  12338  sqrlem6  12678  rlimf  12920  lo1f  12937  lo1dm  12938  o1f  12948  o1dm  12949  fsumge0  13198  mertenslem2  13285  divalglem9  13545  bitsinv2  13579  bitsf1ocnv  13580  gcdcllem1  13635  prmnn  13706  prmind2  13714  nprm  13717  prmuz2  13721  isprm6  13735  exprmfct  13736  isprm5  13738  maxprmfct  13739  phibndlem  13785  phibnd  13786  dfphi2  13789  phimullem  13794  pclem  13845  pcprendvds2  13848  pcpre1  13849  expnprm  13904  prmreclem1  13917  1arith  13928  4sqlem15  13960  4sqlem16  13961  vdwlem5  13986  vdwlem6  13987  vdwlem8  13989  vdwlem9  13990  vdwlem11  13992  ramtlecl  14001  0ramcl  14024  firest  14311  acsmre  14530  posprs  15059  latpos  15160  clatpos  15220  dlatl  15305  pslem  15316  tsrlemax  15330  tsrps  15331  mndlem1  15359  grpmnd  15487  nsgsubg  15650  ghmgrp1  15686  ghmgrp2  15687  gimghm  15729  gagrp  15747  gaset  15748  psgneu  15949  efgredeu  16186  ablgrp  16219  cmnmnd  16229  cyggenod2  16298  cyggrp  16302  ablfac2  16456  crngrng  16483  dvdsrcl  16564  unitcl  16574  drngrng  16652  subrgrng  16681  subrgrcl  16683  srngrhm  16749  lmimlmhm  16954  lveclmod  16996  2idlcpbl  17125  divs1  17126  divsrhm  17128  lpirrng  17143  nzrrng  17152  domnnzr  17175  fldidom  17185  assalmod  17199  assarng  17200  assasca  17201  cygznlem1  17707  cygznlem3  17710  lbslinds  17961  gsummatr01lem1  18165  topontop  18235  tpstop  18248  clsval2  18358  mretopd  18400  neiptoptop  18439  perftop  18464  restfpw  18487  cntop1  18548  cntop2  18549  cnptop1  18550  cnptop2  18551  cnprcl  18553  t1ficld  18635  t0top  18637  t1top  18638  haustop  18639  regtop  18641  nrmtop  18644  cnrmtop  18645  pnrmnrm  18648  cmptop  18702  discmp  18705  tgcmp  18708  uncmp  18710  conndisj  18724  contop  18725  1stctop  18751  llytop  18780  nllytop  18781  hmeocn  19037  filfbas  19125  ufilfil  19181  flimtop  19242  flimfil  19246  alexsublem  19320  ptcmplem3  19330  tsmsfbas  19402  tsmslem1  19403  tsmsgsum  19413  tsmssubm  19417  tsmsres  19418  tsmsf1o  19419  tsmsmhm  19420  tsmsadd  19421  tsmsxplem1  19427  tsmsxplem2  19428  tsmsxp  19429  tlmtmd  19461  tlmlmod  19463  tlmtrg  19464  tvctlm  19471  ressust  19539  uspreg  19549  ucncn  19560  neipcfilu  19571  cuspusp  19575  isxmet2d  19602  metxmet  19609  xmstps  19728  msxms  19729  xmsxmet  19731  msmet  19732  stdbdxmet  19790  nrgngp  19943  nlmngp  19958  nlmlmod  19959  nlmnrg  19960  nvcnlm  19976  nmoi  20007  nghmrcl1  20011  nghmrcl2  20012  nmhmrcl1  20026  nmhmrcl2  20027  qdensere  20049  xrge0gsumle  20110  xrge0tsms  20111  metds0  20126  metdstri  20127  metdsre  20129  metdseq0  20130  metdscnlem  20131  metnrmlem1a  20134  metnrmlem1  20135  icopnfcnv  20214  icopnfhmeo  20215  cvsclm  20379  cmetmet  20497  cmsms  20559  hlbn  20575  ovolicc1  20699  ovolicc2lem5  20704  mblss  20714  mbff  20805  mbfres  20822  mbfadd  20839  mbfsub  20840  i1fmbf  20853  mbfmul  20904  bddmulibl  21016  limcmpt  21058  c1liplem1  21168  c1lip2  21170  fta1glem1  21378  fta1glem2  21379  fta1g  21380  fta1b  21382  ply1pid  21392  aacn  21524  ulmf2  21590  logdmnrp  21827  logdmss  21828  logcnlem2  21829  logcnlem3  21830  logcnlem4  21831  logcnlem5  21832  logcn  21833  dvloglem  21834  logf1o2  21836  efopnlem1  21842  logtayl2  21848  cxpcn  21924  cxpcn3lem  21926  cxpcn3  21927  resqrcn  21928  atandmneg  22042  atandmcj  22045  cosatan  22057  cosatanne0  22058  birthdaylem1  22086  areacl  22097  cxp2lim  22111  jensenlem2  22122  jensen  22123  wilth  22150  sqff1o  22261  dvdsmulf1o  22275  mersenne  22307  bposlem3  22366  lgsqrlem1  22421  lgsqrlem2  22422  lgsqrlem3  22423  lgsqrlem4  22424  lgseisenlem3  22431  lgsquad2lem2  22439  2sqlem6  22449  chebbnd1  22462  chtppilim  22465  chpchtlim  22469  chpo1ub  22470  rplogsumlem1  22474  rplogsumlem2  22475  dchrmusumlema  22483  dchrvmasumiflem1  22491  dchrisum0flblem2  22499  dchrisum0lema  22504  dchrisum0lem2  22508  selberg3lem2  22548  pntrsumo1  22555  selbergsb  22565  pnt2  22603  ostthlem2  22618  ostth2lem2  22624  tglineeltr  22764  axcontlem2  22890  axcontlem7  22895  axcontlem8  22896  axcontlem10  22898  uhgra0v  22923  usgra0v  22969  usgra1v  22987  eupagra  23266  ablogrpo  23450  smgrpismgm  23498  mndoissmgrp  23505  nmogtmnf  23849  bnnv  23946  hlobn  23968  hcauseq  24266  hlimseqi  24270  hlimveci  24271  shss  24291  sh0  24297  chsh  24306  lnopf  24942  bdopln  24944  nmopgtmnf  24951  hmopf  24957  lnfnf  24967  unopf1o  24999  elunop2  25096  elpjhmop  25268  stcltrlem1  25359  mdslle1i  25400  mdslle2i  25401  rabexgfGS  25566  suppss3  25707  ssnnssfz  25754  tospos  25797  ogrpgrp  25845  ogrpinvOLD  25857  ogrpinv0le  25858  ogrpsub  25859  ogrpaddlt  25860  archirng  25884  archirngz  25885  archiabllem1a  25887  archiabllem1b  25888  archiabllem1  25889  archiabllem2a  25890  archiabllem2c  25891  archiabllem2b  25892  archiabllem2  25893  xrge0tsmsd  25961  ofldfld  25986  ofldlt1  25989  ofldchr  25990  isarchiofld  25993  reofld  26017  rearchi  26019  lmxrge0  26091  qqhrhm  26127  esumpcvgval  26236  measssd  26338  elmbfmvol2  26391  sibfinima  26428  eulerpartlemr  26460  eulerpartlemgf  26465  fiblem  26484  domprobmeas  26496  ballotlemscr  26604  ballotlemfg  26611  ballotlemfrc  26612  ballotlemfrceq  26614  ballotlemrinv0  26618  signstfveq0  26681  subfacval3  26780  pcontop  26817  sconpcon  26819  cvmcn  26854  cvmliftlem10  26886  fundmpss  27279  predel  27346  sltres  27507  funpartfun  27676  outsideofcol  27866  itg2addnc  28117  itg2gt0cn  28118  ftc1anclem3  28140  fnebas  28216  filnetlem3  28272  istotbnd3  28341  totbndmet  28342  sstotbnd2  28344  sstotbnd  28345  equivtotbnd  28348  bndmet  28351  totbndbnd  28359  prdstotbnd  28364  crngorngo  28471  prrngorngo  28522  divrngpr  28524  an3  28667  nacsacs  28717  eldiophelnn0  28775  jm2.17a  28976  jm2.17b  28977  jm2.17c  28978  jm2.27c  29029  jm3.1lem1  29039  jm3.1lem2  29040  jm3.1lem3  29041  lnmlmod  29105  lnrrng  29141  mncply  29167  idomrootle  29233  idomodle  29234  hashgcdlem  29238  areaquad  29265  stoweidlem14  29483  stoweidlem16  29485  stoweidlem24  29493  stoweidlem39  29508  stoweidlem50  29519  stoweidlem51  29520  stoweidlem54  29523  stoweidlem57  29526  wallispilem3  29536  ndmafv  29720  rusgranumwlks  30248  frgrawopreg  30316  2uasbanh  30847  bnj563  31313  bnj658  31321  bnj667  31322  bnj570  31476  bnj938  31508  bnj1001  31529  bnj1006  31530  bnj1049  31543  bnj1121  31554  bnj1173  31571  bnj1177  31575  bnj1245  31583  bnj1311  31593  bnj1321  31596  bnj1388  31602  bnj1398  31603  bnj1415  31607  bnj1417  31610  bnj1421  31611  bnj1442  31618  bnj1452  31621  bnj1489  31625  bnj1312  31627  ollat  32295  omlol  32322  cvlatl  32407  hlomcmcv  32438  2dim  32551  1dimN  32552  lcfl8b  34586  lclkrlem2  34614  lclkrslem1  34619  lclkrslem2  34620  lcfrlem9  34632  mapdval2N  34712  mapdordlem2  34719  mapdrvallem2  34727
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 179  df-an 364
  Copyright terms: Public domain W3C validator