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

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

Proof of Theorem simprbi
StepHypRef Expression
1 simprbi.1 . . 3
21biimpi 194 . 2
32simprd 463 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  xornan  1371  sb1  1742  eumo  2313  2eu1OLD  2377  reurmo  3075  pssne  3599  pssn2lp  3604  ssnpss  3606  eldifn  3626  rabsnt  4107  eldifsni  4156  unimax  4285  ssintub  4304  reusv6OLD  4663  moop2  4747  pwssun  4791  weso  4875  ordwe  4896  opelxp2  5038  eldmeldmressn  5319  funmo  5609  funopg  5625  funun  5635  fununi  5659  funimaexg  5670  fndm  5685  frn  5742  f1ss  5791  f1ssr  5792  f1ssres  5793  forn  5803  f1f1orn  5832  f1orescnv  5836  f1imacnv  5837  funcocnv2  5845  dffv2  5946  exfo  6049  foelrn  6050  isorel  6222  isoini2  6235  f1ofveu  6291  fovcl  6407  f1opw  6529  onminesb  6633  onminsb  6634  tfis  6689  limomss  6705  nnlim  6713  ssnlim  6718  curry1  6892  curry2  6895  f1o2ndf1  6908  fnwelem  6915  ressuppss  6938  mpt2xopn0yelv  6960  tz7.48lem  7125  dif20el  7174  oeordi  7255  oeeulem  7269  oeeui  7270  nnawordex  7305  swoer  7358  erdisj  7378  eceqoveq  7435  mapsnconst  7484  ixpn0  7521  resixpfo  7527  boxcutc  7532  sdomnen  7564  en0  7598  en1  7602  domunsncan  7637  fodomr  7688  phplem4  7719  php3  7723  unxpdomlem3  7746  fineqvlem  7754  f1opwfi  7844  fsuppcolem  7880  fsuppco  7881  mapfienlem1  7884  mapfienlem2  7885  supub  7939  suplub  7940  ordtypelem2  7965  ordtypelem3  7966  ordtypelem6  7969  ordtypelem7  7970  wemapso2OLD  7998  wemapso2lem  7999  wdom2d  8027  brwdom3  8029  ixpiunwdom  8038  inf3lem2  8067  inf3lem6  8071  oancom  8089  infdifsn  8094  cantnfp1lem3  8120  cantnflem3  8131  cantnflem4  8132  cantnfp1lem3OLD  8146  cantnflem3OLD  8153  cantnflem4OLD  8154  cantnfOLD  8155  mapfienOLD  8159  oef1o  8162  oef1oOLD  8163  cnfcom3  8169  cnfcomlemOLD  8172  cnfcom3OLD  8177  tctr  8192  tz9.12lem3  8228  scottex  8324  cardid2  8355  infxpenlem  8412  acni3  8449  cardaleph  8491  iscard3  8495  dfac5lem4  8528  dfac5lem5  8529  kmlem1  8551  cofsmo  8670  fin4en1  8710  enfin2i  8722  fin23lem28  8741  fin23lem38  8750  isf32lem6  8759  enfin1ai  8785  isfin1-3  8787  hsmexlem2  8828  hsmexlem4  8830  domtriomlem  8843  axdc2lem  8849  axdc3lem2  8852  ac6num  8880  zorn2lem2  8898  brdom3  8927  alephval2  8968  alephreg  8978  pwcfsdom  8979  smobeth  8982  fpwwe2lem6  9034  fpwwe2lem13  9041  canthp1lem2  9052  pwfseqlem3  9059  hargch  9072  winalim2  9095  gchina  9098  inar1  9174  0npi  9281  mulclpi  9292  mulcanpi  9299  nlt1pi  9305  nqereu  9328  prcdnq  9392  prnmax  9394  ltresr2  9539  axrnegex  9560  axpre-sup  9567  1nuz2  11186  zsupss  11200  rpgt0  11260  ixxss1  11576  ixxss2  11577  ixxss12  11578  lbioo  11589  ubioo  11590  iccss2  11624  iccssico2  11627  elfzuz3  11714  uzdisj  11780  nn0disj  11820  serge0  12161  expge0  12202  expge1  12203  expaddzlem  12209  hashrabsn1  12442  hashfun  12495  shftfn  12906  sqrlem6  13081  rlimss  13325  lo1dm  13342  o1dm  13353  rlimrege0  13402  fsumf1o  13545  fsumge0  13609  incexc2  13650  supcvg  13667  fprodf1o  13753  divalglem9  14059  bitsfzolem  14084  bitsinv2  14093  bitsf1ocnv  14094  bitsf1  14096  gcdcllem1  14149  bezout  14180  prmind2  14228  nprm  14231  sqnprm  14239  dvdsprm  14240  coprm  14241  isprm5  14253  phibndlem  14300  dfphi2  14304  phimullem  14309  pclem  14362  pcpre1  14366  pcidlem  14395  expnprm  14421  prmreclem1  14434  prmreclem2  14435  prmreclem5  14438  1arith  14445  4sqlem18  14480  vdwnnlem3  14515  ramtlecl  14518  rami  14533  0ram  14538  ramub1lem1  14544  firest  14830  acsfiel  15051  isacs1i  15054  catlid  15080  catrid  15081  fullfo  15281  fthf1  15286  fthoppc  15292  invfuc  15343  prslem  15560  posi  15579  dlatmjdi  15824  pslem  15836  tsrlin  15849  cnvtsr  15852  tsrdir  15868  mndid  15933  mhmf  15971  mhmlin  15973  mhm0  15974  mrcmndind  15997  grpinvex  16065  grplinv  16096  mulgz  16163  mulgdirlem  16166  mulgdir  16167  mulgass  16172  nsgbi  16232  nmzbi  16241  ghmf  16271  ghmlin  16272  conjnsg  16302  gimf1o  16311  gagrpid  16332  gaf  16333  gaass  16335  psgnunilem5  16519  odid  16562  odf1o2  16593  gexid  16601  sylow1lem4  16621  odcau  16624  pj1id  16717  efgredeu  16770  ablcmn  16804  cmncom  16814  mulgdi  16835  gexexlem  16858  torsubg  16860  cyggenod2  16888  cygctb  16894  ghmcyg  16898  dprdf1o  17079  dprd2dlem1  17090  dprd2da  17091  ablfacrplem  17116  ablfaclem2  17137  ablfac2  17140  crngmgp  17206  rhmmhm  17371  rhmghm  17374  drngunit  17401  drngmgp  17408  drngid  17410  subrgss  17430  subrg1cl  17437  issubdrg  17454  abvge0  17474  srngcnv  17502  lmhmlin  17681  lmimf1o  17709  lvecdrng  17751  lspsolvlem  17788  islbs3  17801  lbsextlem3  17806  2idlcpbl  17882  nzrnz  17908  opprnzr  17913  rrgeq0i  17937  domneq0  17946  domnrrg  17949  drngdomn  17952  fldidom  17954  assalem  17965  mplsubrglem  18100  mplsubrglemOLD  18101  mplcoe1  18127  mplbas2  18134  mplbas2OLD  18135  opsrtoslem2  18149  mplelsfi  18155  mplelsfiOLD  18156  coe1mul2  18310  zringunit  18520  zrngunit  18521  prmirredlem  18523  prmirredlemOLD  18526  znidomb  18600  cygzn  18609  psgndiflemB  18636  pjf  18744  frlmsslsp  18829  frlmsslspOLD  18830  frlmlbs  18831  f1lindf  18857  pmatcoe1fsupp  19202  toponuni  19428  tpsuni  19439  clsval2  19551  mretopd  19593  neips  19614  neiptoptop  19632  neiptopnei  19633  perflp  19655  perfi  19656  restfpw  19680  cnf  19747  cnpf  19748  cnpimaex  19757  cnima  19766  t0sep  19825  t1sncld  19827  t1ficld  19828  hausnei  19829  regsep  19835  pnrmcld  19843  nrmsep3  19856  cnrmi  19861  cmpcov  19889  discmp  19898  tgcmp  19901  uncmp  19903  hauscmplem  19906  cmpfi  19908  conclo  19916  1stcclb  19945  2ndcdisj  19957  llyi  19975  nllyi  19976  ptpjpre1  20072  ptpjcn  20112  ptpjopn  20113  ptclsg  20116  dfac14  20119  txdis1cn  20136  pthaus  20139  hauseqlcld  20147  txkgen  20153  xkococn  20161  txcon  20190  hmeocnvcn  20262  fbssfi  20338  filss  20354  ufilss  20406  uffixfr  20424  flimneiss  20467  flimelbas  20469  fclscf  20526  flimfnfcls  20529  alexsublem  20544  alexsubb  20546  alexsubALT  20551  ptcmplem2  20553  ptcmplem3  20554  ptcmplem4  20555  tmdgsum2  20595  ghmcnp  20613  tgpt0  20617  qustgplem  20619  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  istdrg2  20680  vscacn  20688  tvctdrg  20695  uspreg  20777  ucncn  20788  neipcfilu  20799  cuspcvg  20804  psmetxrge0  20817  isxmet2d  20830  prdsxmetlem  20871  imasdsf1olem  20876  xmstopn  20954  mstopn  20955  stdbdxmet  21018  prdsxmslem2  21032  nrgabv  21170  nmvs  21185  nvclvec  21205  nmoge0  21228  nghmcl  21234  nmoi  21235  nghmghm  21241  nmhmlmhm  21256  nmhmnghm  21257  icccmp  21330  xrge0gsumle  21338  xrge0tsms  21339  metds0  21354  metdstri  21355  metdsre  21357  metdseq0  21358  metdscnlem  21359  metnrmlem1a  21362  icopnfcnv  21442  xrhmeo  21446  pcoval1  21513  cvslvec  21606  cvsunit  21608  cphreccllem  21625  cmetcvg  21724  lmle  21740  cmscmet  21785  cmetcusp1OLD  21791  cmetcusp1  21792  hlcph  21804  minveclem4  21847  ivthlem3  21865  ovolmge0  21888  ovolicc1  21927  ovolicc2lem3  21930  ovolicc2lem5  21932  mblsplit  21943  dyadmbl  22009  mbfdm  22035  mbfadd  22068  mbfsub  22069  i1ff  22083  i1frn  22084  i1fima2  22086  mbfmul  22133  itg2monolem1  22157  bddmulibl  22245  dvnres  22334  c1liplem1  22397  c1lip2  22399  dvge0  22407  lhop1lem  22414  itgsubstlem  22449  fta1glem1  22566  fta1glem2  22567  fta1b  22570  plyf  22595  plypf1  22609  plyadd  22614  plymul  22615  coeeu  22622  dgrlem  22626  coeid  22635  elqaalem3  22717  aareccl  22722  eff1olem  22935  relogf1o  22954  logdmn0  23021  logcnlem2  23024  logcnlem3  23025  dvloglem  23029  efopnlem1  23037  efopnlem2  23038  logtayl2  23043  cxpcn3lem  23121  cxpcn3  23122  atandmneg  23237  atandmcj  23240  efiatan2  23248  cosatan  23252  cosatanne0  23253  dvatan  23266  areage0  23293  cxp2lim  23306  jensenlem2  23317  jensen  23318  wilthlem1  23342  wilth  23345  ftalem3  23348  efnnfsumcl  23376  isppw  23388  efchtdvds  23433  sqff1o  23456  dvdsdivcl  23457  fsumdvdsdiaglem  23459  dvdsppwf1o  23462  dvdsflf1o  23463  musum  23467  muinv  23469  dvdsmulf1o  23470  fsumvma2  23489  vmasum  23491  chpval2  23493  chpchtsum  23494  chpub  23495  mersenne  23502  perfect1  23503  bposlem1  23559  bposlem5  23563  lgsfle1  23580  lgsle1  23586  lgsdirprm  23604  lgsne0  23608  lgsqrlem4  23619  lgseisenlem3  23626  lgseisenlem4  23627  lgsquadlem1  23629  lgsquadlem2  23630  2sqblem  23652  chebbnd1lem1  23654  chebbnd1  23657  chtppilim  23660  chpchtlim  23664  chpo1ub  23665  rplogsumlem2  23670  rpvmasumlem  23672  dchrmusumlema  23678  dchrvmasumlem1  23680  dchrisum0flblem2  23694  dchrisum0lema  23699  dchrisum0lem2a  23702  logsqvma  23727  selberg3lem2  23743  pntrsumo1  23750  pnt2  23798  ostthlem1  23812  ostth3  23823  axtgcgrrflx  23859  axtgcgrid  23860  axtgsegcon  23861  axtg5seg  23862  axtgbtwnid  23863  axtgpasch  23864  axtgcont1  23865  tglng  23933  axcontlem7  24273  axcontlem10  24276  umgrale  24321  usgraedg2  24375  usgraexmpledg  24403  clwlkfclwwlk1hashn  24841  eupatrl  24968  gxneg  25268  gxadd  25277  gxmul  25280  ablocom  25287  subgoablo  25313  smgrpisass  25335  mndoisexid  25342  zrdivrng  25434  phpar2  25738  cbncms  25781  hlph  25805  hcaucvg  26103  hlimconvi  26108  shaddcl  26134  shmulcl  26135  shmulclOLD  26136  chlimi  26152  chcompl  26160  choc1  26245  nmopre  26789  cnopc  26832  lnopl  26833  unop  26834  hmop  26841  cnfnc  26849  lnfnl  26850  nlelshi  26979  cnlnadjlem5  26990  elpjidm  27103  mdslle1i  27236  mdslle2i  27237  atcv0  27261  chpssati  27282  fovcld  27478  ssnnssfz  27597  ressprs  27643  oduprs  27644  resspos  27647  resstos  27648  tleile  27649  ogrpinvOLD  27705  ogrpinv0le  27706  ogrpsub  27707  ogrpaddlt  27708  isarchi3  27731  archirng  27732  archirngz  27733  archiabllem1a  27735  archiabllem1b  27736  archiabllem2a  27738  archiabllem2c  27739  archiabllem2b  27740  archiabl  27742  xrge0tsmsd  27775  orngsqr  27794  ornglmulle  27795  orngrmulle  27796  ofldtos  27801  ofldlt1  27803  ofldchr  27804  suborng  27805  subofld  27806  isarchiofld  27807  nn0omnd  27831  qtophaus  27839  crefi  27850  cmpcref  27853  cmppcmp  27861  pcmplfin  27863  tpr2rico  27894  rge0scvg  27931  zrhunitpreima  27959  qqhrhm  27970  esummono  28066  gsumesum  28067  esumpinfval  28079  esumpcvgval  28084  esumpmono  28085  0elsiga  28114  sigaclcu  28117  issgon  28123  sxuni  28164  isrnmeas  28171  measvuni  28185  measssd  28186  ddemeas  28208  imambfm  28233  elmbfmvol2  28238  dya2icoseg2  28249  sibfinima  28281  oddpwdc  28293  oddpwdcv  28294  eulerpartlemf  28309  eulerpartlemt  28310  eulerpartlemr  28313  eulerpartlemgvv  28315  eulerpartlemgs2  28319  sseqf  28331  fiblem  28337  probtot  28351  ballotlem4  28437  ballotlem5  28438  ballotlemfrc  28465  ballotlemirc  28470  ballotth  28476  eldmgm  28564  dmgmaddn0  28565  dmlogdmgm  28566  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem5  28575  lgambdd  28579  lgamucov  28580  subfacp1lem3  28626  subfacp1lem5  28628  pconcn  28669  sconpht  28674  conpcon  28680  cvmcov  28708  cvmliftlem1  28730  cvmliftlem10  28739  cvmlift2lem11  28758  cvmlift2lem12  28759  msubff1  28916  mvhf1  28919  mthmpps  28942  mclspps  28944  fundmpss  29196  tfisg  29284  wfisg  29289  frinsg  29325  wfrlem5  29347  frrlem5  29391  sltval2  29416  txpss3v  29528  pprodss4v  29534  onint1  29914  wl-nfeqfb  29990  fin2solem  30039  fin2so  30040  ptrest  30048  mblfinlem2  30052  dvtan  30065  itg2gt0cn  30070  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  fnetg  30163  neibastop1  30177  filnetlem3  30198  cover2  30204  indexa  30224  istotbnd3  30267  sstotbnd2  30270  sstotbnd  30271  totbndss  30273  equivtotbnd  30274  isbnd3  30280  totbndbnd  30285  equivbnd  30286  prdsbnd  30289  prdstotbnd  30290  heibor  30317  crngocom  30398  isfld2  30402  dmncrng  30453  prter2  30622  nacsfg  30637  nacsfix  30644  mzpindd  30678  diophrw  30692  diophrex  30709  rexzrexnn0  30737  pell1234qrdich  30797  rmspecsqrtnq  30842  rmspecnonsq  30843  rmspecfund  30845  rmspecpos  30852  monotoddzzfi  30878  ltrmxnn0  30887  rmxnn  30889  jm2.23  30938  jm3.1lem2  30960  dnnumch3  30993  lnmlssfg  31026  lnmlmic  31034  lnrlnm  31062  lnr2i  31065  lpirlnr  31066  hbtlem6  31078  hbt  31079  mnccoe  31087  cntzsdrg  31151  idomrootle  31152  proot1mul  31156  phisum  31159  proot1hash  31160  deg1mhm  31167  radcnvrat  31195  binomcxplemdvbinom  31258  binomcxplemcvg  31259  binomcxplemnotnn0  31261  elinel2  31423  sumnnodd  31636  stoweidlem7  31789  stoweidlem14  31796  stoweidlem16  31798  stoweidlem24  31806  stoweidlem31  31813  stoweidlem54  31836  wallispilem3  31849  fourierdlem42  31931  fourierdlem48  31937  fourierdlem51  31940  fourierdlem64  31953  fourierdlem76  31965  fourierdlem79  31968  fourierdlem81  31970  fourierdlem87  31976  etransclem28  32045  etransclem32  32049  2reu1  32191  nfunsnafv  32227  faovcl  32285  usgra2pth  32354  clintopcllaw  32535  0ringbas  32677  rnghmmgmhm  32700  uzlidlring  32735  rnghmsubcsetclem1  32783  rngccatidOLD  32797  zrinitorngc  32808  zrtermorngc  32809  rhmsubcsetclem1  32829  funcringcsetcOLD2lem7  32850  ringccatidOLD  32860  funcringcsetclem7OLD  32873  irinitoringc  32877  zrtermoringc  32878  fldhmsubc  32892  fldhmsubcOLD  32911  ssnn0ssfz  32938  el0ldepsnzr  33068  ordelordALT  33308  2uasbanh  33334  ordelordALTVD  33667  bnj642  33805  bnj643  33806  bnj645  33807  bnj707  33812  bnj1379  33889  bnj1538  33913  bnj110  33916  bnj93  33921  bnj906  33988  bnj1006  34017  bnj1110  34038  bnj1121  34041  bnj1172  34057  bnj1204  34068  bnj1321  34083  bnj1364  34084  bnj1398  34090  bnj1450  34106  bnj1312  34114  bnj1501  34123  bnj1523  34127  bj-elid2  34600  toycom  34698  lsateln0  34720  lpssat  34738  lssat  34741  oposlem  34907  olop  34939  omllaw  34968  cvlexch1  35053  dihpN  37063  mapdordlem2  37364
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