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

Theorem simplbi 448
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 447 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360
This theorem is referenced by:  3simpa  959  sbequ2  1678  reurex  2980  eqimss  3445  pssss  3488  eldifi  3515  inss1  3606  ssunsn2  4058  pwssun  4648  sopo  4679  wefr  4731  ordtr  4754  opelxp1  4894  relop  5012  funmo  5454  funrel  5455  fnfun  5526  ffn  5577  f1f  5623  f1of1  5657  f1ofo  5665  isof1o  6026  eqopi  6616  1st2nd2  6619  reldmtpos  6719  swoer  7095  erdisj  7114  ecopover  7170  sdomdom  7299  inf3lemd  7749  mapfien  7820  cardprclem  8035  infxpenlem  8066  cardinfima  8149  dfac5lem4  8178  domtriomlem  8493  smobeth  8632  fpwwe2lem6  8681  fpwwe2lem7  8682  fpwwe2lem12  8687  fpwwe2lem13  8688  fpwwe2  8689  axrnegex  9208  axpre-sup  9215  zre  10514  nnssz  10530  ixxss1  11182  ixxss2  11183  ixxss12  11184  lbioo  11195  ubioo  11196  iccss2  11229  elfzuz  11305  uzdisj  11383  0wrd0  12100  splfv1  12244  sqrlem6  12584  rlimf  12826  lo1f  12843  lo1dm  12844  o1f  12854  o1dm  12855  fsumge0  13105  mertenslem2  13192  divalglem9  13452  bitsinv2  13486  bitsf1ocnv  13487  gcdcllem1  13542  prmnn  13613  prmind2  13621  nprm  13624  prmuz2  13628  isprm6  13642  exprmfct  13643  isprm5  13645  maxprmfct  13646  phibndlem  13692  phibnd  13693  dfphi2  13696  phimullem  13701  pclem  13752  pcprendvds2  13755  pcpre1  13756  expnprm  13811  prmreclem1  13824  1arith  13835  4sqlem15  13867  4sqlem16  13868  vdwlem5  13893  vdwlem6  13894  vdwlem8  13896  vdwlem9  13897  vdwlem11  13899  ramtlecl  13908  0ramcl  13931  firest  14214  acsmre  14431  posprs  14960  latpos  15061  clatpos  15121  dlatl  15206  pslem  15217  tsrlemax  15231  tsrps  15232  mndlem1  15260  grpmnd  15388  nsgsubg  15543  ghmgrp1  15579  ghmgrp2  15580  gimghm  15622  gagrp  15640  gaset  15641  efgredeu  15993  ablgrp  16026  cmnmnd  16036  cyggenod2  16105  cyggrp  16109  ablfac2  16262  crngrng  16289  dvdsrcl  16370  unitcl  16380  drngrng  16458  subrgrng  16487  subrgrcl  16489  srngrhm  16555  lmimlmhm  16759  lveclmod  16801  2idlcpbl  16930  divs1  16931  divsrhm  16933  lpirrng  16948  nzrrng  16957  domnnzr  16980  fldidom  16990  assalmod  17004  assarng  17005  assasca  17006  cygznlem1  17472  cygznlem3  17475  psgneu  17659  gsummatr01lem1  17935  topontop  18005  tpstop  18018  clsval2  18128  mretopd  18170  neiptoptop  18209  perftop  18234  restfpw  18257  cntop1  18318  cntop2  18319  cnptop1  18320  cnptop2  18321  cnprcl  18323  t1ficld  18405  t0top  18407  t1top  18408  haustop  18409  regtop  18411  nrmtop  18414  cnrmtop  18415  pnrmnrm  18418  cmptop  18472  discmp  18475  tgcmp  18478  uncmp  18480  conndisj  18494  contop  18495  1stctop  18521  llytop  18550  nllytop  18551  hmeocn  18807  filfbas  18895  ufilfil  18951  flimtop  19012  flimfil  19016  alexsublem  19090  ptcmplem3  19100  tsmsfbas  19172  tsmslem1  19173  tsmsgsum  19183  tsmssubm  19187  tsmsres  19188  tsmsf1o  19189  tsmsmhm  19190  tsmsadd  19191  tsmsxplem1  19197  tsmsxplem2  19198  tsmsxp  19199  tlmtmd  19231  tlmlmod  19233  tlmtrg  19234  tvctlm  19241  ressust  19309  uspreg  19319  ucncn  19330  neipcfilu  19341  cuspusp  19345  isxmet2d  19372  metxmet  19379  xmstps  19498  msxms  19499  xmsxmet  19501  msmet  19502  stdbdxmet  19560  nrgngp  19713  nlmngp  19728  nlmlmod  19729  nlmnrg  19730  nvcnlm  19746  nmoi  19777  nghmrcl1  19781  nghmrcl2  19782  nmhmrcl1  19796  nmhmrcl2  19797  qdensere  19819  xrge0gsumle  19879  xrge0tsms  19880  metds0  19895  metdstri  19896  metdsre  19898  metdseq0  19899  metdscnlem  19900  metnrmlem1a  19903  metnrmlem1  19904  icopnfcnv  19982  icopnfhmeo  19983  cmetmet  20254  cmsms  20316  hlbn  20332  ovolicc1  20427  ovolicc2lem5  20432  mblss  20442  mbff  20532  mbfres  20549  mbfadd  20566  mbfsub  20567  i1fmbf  20580  mbfmul  20631  bddmulibl  20743  limcmpt  20785  c1liplem1  20895  c1lip2  20897  fta1glem1  21103  fta1glem2  21104  fta1g  21105  fta1b  21107  ply1pid  21117  aacn  21249  ulmf2  21315  logdmnrp  21552  logdmss  21553  logcnlem2  21554  logcnlem3  21555  logcnlem4  21556  logcnlem5  21557  logcn  21558  dvloglem  21559  logf1o2  21561  efopnlem1  21567  logtayl2  21573  cxpcn  21649  cxpcn3lem  21651  cxpcn3  21652  resqrcn  21653  atandmneg  21767  atandmcj  21770  cosatan  21782  cosatanne0  21783  birthdaylem1  21811  areacl  21822  cxp2lim  21836  jensenlem2  21847  jensen  21848  wilth  21875  sqff1o  21986  dvdsmulf1o  22000  mersenne  22032  bposlem3  22091  lgsqrlem1  22146  lgsqrlem2  22147  lgsqrlem3  22148  lgsqrlem4  22149  lgseisenlem3  22156  lgsquad2lem2  22164  2sqlem6  22174  chebbnd1  22187  chtppilim  22190  chpchtlim  22194  chpo1ub  22195  rplogsumlem1  22199  rplogsumlem2  22200  dchrmusumlema  22208  dchrvmasumiflem1  22216  dchrisum0flblem2  22224  dchrisum0lema  22229  dchrisum0lem2  22233  selberg3lem2  22273  pntrsumo1  22280  selbergsb  22290  pnt2  22328  ostthlem2  22343  ostth2lem2  22349  uhgra0v  22366  usgra0v  22412  usgra1v  22430  eupagra  22709  ablogrpo  22893  smgrpismgm  22941  mndoissmgrp  22948  nmogtmnf  23292  bnnv  23389  hlobn  23411  hcauseq  23709  hlimseqi  23713  hlimveci  23714  shss  23734  sh0  23740  chsh  23749  lnopf  24385  bdopln  24387  nmopgtmnf  24394  hmopf  24400  lnfnf  24410  unopf1o  24442  elunop2  24539  elpjhmop  24711  stcltrlem1  24802  mdslle1i  24843  mdslle2i  24844  rabexgfGS  25014  suppss3  25157  ssnnssfz  25206  tospos  25250  ogrpgrp  25298  ogrpinvOLD  25310  ogrpinv0le  25311  ogrpsub  25312  ogrpaddlt  25313  archirng  25337  archirngz  25338  archiabllem1a  25340  archiabllem1b  25341  archiabllem1  25342  archiabllem2a  25343  archiabllem2c  25344  archiabllem2b  25345  archiabllem2  25346  xrge0tsmsd  25414  ofldfld  25439  ofldlt1  25442  ofldchr  25443  isarchiofld  25446  reofld  25487  rearchi  25489  lmxrge0  25561  qqhrhm  25598  esumpcvgval  25707  measssd  25809  elmbfmvol2  25862  sibfinima  25899  oddpwdcv  25912  eulerpartlemf  25927  eulerpartlemr  25931  eulerpartlemgf  25936  eulerpartlemgs2  25937  domprobmeas  25943  ballotlemscr  26051  ballotlemfg  26058  ballotlemfrc  26059  ballotlemfrceq  26061  ballotlemrinv0  26065  signstfveq0  26129  subfacval3  26223  pcontop  26260  sconpcon  26262  cvmcn  26297  cvmliftlem10  26329  fundmpss  26729  predel  26797  sltres  26958  funpartfun  27127  axcontlem2  27243  axcontlem7  27248  axcontlem8  27249  axcontlem10  27251  outsideofcol  27406  itg2addnc  27626  itg2gt0cn  27627  ftc1anclem3  27649  fnebas  27725  filnetlem3  27781  istotbnd3  27852  totbndmet  27853  sstotbnd2  27855  sstotbnd  27856  equivtotbnd  27859  bndmet  27862  totbndbnd  27870  prdstotbnd  27875  crngorngo  27982  prrngorngo  28033  divrngpr  28035  an3  28139  nacsacs  28193  eldiophelnn0  28250  jm2.17a  28451  jm2.17b  28452  jm2.17c  28453  jm2.27c  28504  jm3.1lem1  28514  jm3.1lem2  28515  jm3.1lem3  28516  lnmlmod  28580  lbslinds  28643  lnrrng  28656  mncply  28682  idomrootle  28742  idomodle  28743  hashgcdlem  28747  stoweidlem14  28988  stoweidlem16  28990  stoweidlem24  28998  stoweidlem39  29013  stoweidlem50  29024  stoweidlem51  29025  stoweidlem54  29028  stoweidlem57  29031  wallispilem3  29041  ndmafv  29225  rusgranumwlks  29755  frgrawopreg  29823  2uasbanh  30116  bnj563  30581  bnj658  30589  bnj667  30590  bnj570  30746  bnj938  30778  bnj1001  30799  bnj1006  30800  bnj1049  30813  bnj1121  30824  bnj1173  30841  bnj1177  30845  bnj1245  30853  bnj1311  30863  bnj1321  30866  bnj1388  30872  bnj1398  30873  bnj1415  30877  bnj1417  30880  bnj1421  30881  bnj1442  30888  bnj1452  30891  bnj1489  30895  bnj1312  30897  ollat  31561  omlol  31588  cvlatl  31673  hlomcmcv  31704  2dim  31817  1dimN  31818  lcfl8b  33852  lclkrlem2  33880  lclkrslem1  33885  lclkrslem2  33886  lcfrlem9  33898  mapdval2N  33978  mapdordlem2  33985  mapdrvallem2  33993
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 362
  Copyright terms: Public domain W3C validator