Theorem simprbi 498

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simprbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simprbi	⊢ (𝜑 → 𝜒)

Proof of Theorem simprbi

Step	Hyp	Ref	Expression
1		simprbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 215	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 497	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  simplbiim  506  xornan  1519  eumo  2573  reurmo  3380  pssne  4097  pssn2lp  4102  ssnpss  4104  eldifn  4128  elinel2  4197  rabsnt  4736  eldifsni  4794  unimax  4949  ssintub  4971  moop2  5503  pwssun  5572  weso  5668  opelxp2  5720  predpo  6325  frpoinsg  6345  wfisgOLD  6356  ordwe  6378  funmo  6564  funmoOLD  6565  funopg  6583  funun  6595  fununi  6624  funimaexg  6635  fndm  6653  frn  6725  f1ss  6794  f1ssr  6795  forn  6809  f1f1orn  6845  f1orescnv  6849  f1imacnv  6850  funcocnv2  6859  dffv2  6987  exfo  7107  foelrn  7108  isorel  7323  isoini2  7336  f1ofveu  7403  fovcld  7536  onminesb  7781  onminsb  7782  tfisg  7843  tfis  7844  limomss  7860  nnlim  7869  ssnlim  7875  curry1  8090  curry2  8093  f1o2ndf1  8108  fnwelem  8117  mpoxopn0yelv  8198  wfrlem5OLD  8313  tz7.48lem  8441  dif20el  8505  oeordi  8587  oeeulem  8601  oeeui  8602  nnawordex  8637  swoer  8733  eceqoveq  8816  mapsnconst  8886  resixpfo  8930  boxcutc  8935  sdomnen  8977  en0  9013  en0OLD  9014  en0ALT  9015  en0r  9016  en1  9021  en1OLD  9022  dom0  9102  fodomr  9128  dif1enlem  9156  dif1enlemOLD  9157  unxpdomlem3  9252  fineqvlem  9262  infn0  9307  f1opwfi  9356  fsuppcolem  9396  fsuppco  9397  mapfienlem1  9400  mapfienlem2  9401  supub  9454  suplub  9455  ordtypelem2  9514  ordtypelem3  9515  ordtypelem6  9518  ordtypelem7  9519  wemapso2lem  9547  wdom2d  9575  brwdom3  9577  ixpiunwdom  9585  inf3lem2  9624  inf3lem6  9628  oancom  9646  infdifsn  9652  cantnfp1lem3  9675  cantnflem3  9686  cantnflem4  9687  oef1o  9693  cnfcom3  9699  tctr  9735  frinsg  9746  tz9.12lem3  9784  scottex  9880  cardid2  9948  infxpenlem  10008  acni3  10042  cardaleph  10084  iscard3  10088  dfac5lem4  10121  dfac5lem5  10122  kmlem1  10145  cofsmo  10264  fin4en1  10304  enfin2i  10316  fin23lem28  10335  fin23lem38  10344  isf32lem6  10353  enfin1ai  10379  hsmexlem2  10422  hsmexlem4  10424  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  ac6num  10474  zorn2lem2  10492  brdom3  10523  alephval2  10567  alephreg  10577  pwcfsdom  10578  smobeth  10581  fpwwe2lem5  10630  fpwwe2lem12  10637  canthp1lem2  10648  pwfseqlem3  10655  hargch  10668  winalim2  10691  gchina  10694  inar1  10770  0npi  10877  mulclpi  10888  mulcanpi  10895  nlt1pi  10901  nqereu  10924  prcdnq  10988  prnmax  10990  ltresr2  11136  axrnegex  11157  axpre-sup  11164  eluz2gt1  12904  1nuz2  12908  zsupss  12921  rpgt0  12986  ixxss1  13342  ixxss2  13343  ixxss12  13344  lbioo  13355  ubioo  13356  iccss2  13395  iccssico2  13398  elfzuz3  13498  serge0  14022  expge0  14064  expge1  14065  expaddzlem  14071  hashrabsn1  14334  hashfun  14397  cshinj  14761  relexpuzrel  14999  shftfn  15020  01sqrexlem6  15194  rlimss  15446  lo1dm  15463  o1dm  15474  rlimrege0  15523  fsumf1o  15669  fsumge0  15741  incexc2  15784  supcvg  15802  fprodf1o  15890  divalglem9  16344  bitsfzolem  16375  bitsf1  16387  gcdcllem1  16440  bezout  16485  nprm  16625  dvdsprm  16640  coprm  16648  dfphi2  16707  phimullem  16712  phisum  16723  expnprm  16835  prmreclem2  16850  prmreclem5  16853  1arith  16860  4sqlem18  16895  vdwnnlem3  16930  ramtlecl  16933  rami  16948  0ram  16953  ramub1lem1  16959  prmgaplem5  16988  acsfiel  17598  isacs1i  17601  catlid  17627  catrid  17628  fullfo  17863  fthf1  17868  fthoppc  17874  invfuc  17927  prslem  18251  posi  18270  tleile  18374  dlatmjdi  18476  pslem  18525  tsrlin  18538  cnvtsr  18541  tsrdir  18557  mndid  18635  mhmf  18677  mhmlin  18679  mhm0  18680  mndind  18709  grpinvex  18829  grplinv  18874  mulgz  18982  mulgdirlem  18985  mulgdir  18986  mulgass  18991  nsgbi  19037  nmzbi  19044  ghmf  19096  ghmlin  19097  conjnsg  19128  gimf1o  19137  gagrpid  19158  gaf  19159  gaass  19161  psgnunilem5  19362  odid  19406  odf1o2  19441  gexid  19449  sylow1lem4  19469  pj1id  19567  efgredeu  19620  ablcmn  19655  cmncom  19666  mulgdi  19694  torsubg  19722  cyggenod2  19753  cygctb  19760  ghmcyg  19764  dprdf1o  19902  ablfacrplem  19935  ablfaclem2  19956  ablfac2  19959  simpg2nsg  19966  fincygsubgodexd  19983  crngmgp  20064  rhmmhm  20258  rhmghm  20262  rimf1o  20272  nzrnz  20294  opprnzr  20299  subrgss  20320  subrg1cl  20327  drngunit  20362  fldcrngd  20370  drngmgp  20373  drngid  20375  issubdrg  20401  fldsdrgfld  20414  cntzsdrg  20418  abvge0  20433  srngcnv  20461  lmhmlin  20646  lmimf1o  20674  lvecdrng  20716  lspsolvlem  20755  islbs3  20768  lbsextlem3  20773  2idlelbas  20870  2idlcpbl  20871  rrgeq0i  20905  domneq0  20913  domnrrg  20916  drngdomn  20921  fldidomOLD  20924  zringunit  21036  prmirredlem  21042  znidomb  21117  cygzn  21126  psgndiflemB  21153  pjf  21268  frlmsslsp  21351  frlmlbs  21352  f1lindf  21377  assalem  21412  psrbaglefi  21485  mplelsfi  21554  mplsubrglem  21563  mplcoe1  21592  mplbas2  21597  opsrtoslem2  21617  mhpmulcl  21692  coe1mul2  21791  pmatcoe1fsupp  22203  toponuni  22416  tpsuni  22438  mretopd  22596  neips  22617  neiptoptop  22635  neiptopnei  22636  perflp  22658  perfi  22659  cnf  22750  cnpf  22751  cnpimaex  22760  cnima  22769  t0sep  22828  t1ficld  22831  hausnei  22832  pnrmcld  22846  cnrmi  22864  cmpcov  22893  tgcmp  22905  hauscmplem  22910  connclo  22919  1stcclb  22948  2ndcdisj  22960  llyi  22978  nllyi  22979  ptpjpre1  23075  ptpjcn  23115  ptpjopn  23116  ptclsg  23119  dfac14  23122  txdis1cn  23139  pthaus  23142  hauseqlcld  23150  txkgen  23156  xkococn  23164  txconn  23193  hmeocnvcn  23265  fbssfi  23341  filss  23357  uffixfr  23427  flimneiss  23470  flimelbas  23472  flimfnfcls  23532  alexsubb  23550  alexsubALT  23555  ptcmplem2  23557  ptcmplem3  23558  ptcmplem4  23559  tmdgsum2  23600  ghmcnp  23619  tgpt0  23623  qustgplem  23625  istdrg2  23682  vscacn  23690  tvctdrg  23697  uspreg  23779  ucncn  23790  neipcfilu  23801  cuspcvg  23806  psmetxrge0  23819  isxmet2d  23833  prdsxmetlem  23874  imasdsf1olem  23879  xmstopn  23957  mstopn  23958  stdbdxmet  24024  prdsxmslem2  24038  nrgabv  24178  nmvs  24193  nvclvec  24214  nmoge0  24238  nghmcl  24244  nmoi  24245  nghmghm  24251  nmhmlmhm  24266  nmhmnghm  24267  icccmp  24341  xrge0gsumle  24349  metds0  24366  metdstri  24367  metdsre  24369  metdseq0  24370  metdscnlem  24371  metnrmlem1a  24374  icopnfcnv  24458  xrhmeo  24462  pcoval1  24529  cvslvec  24641  cvsunit  24647  recvs  24662  cphreccllem  24695  cphsscph  24768  cmetcvg  24802  lmle  24818  cmscmet  24863  cmetcusp1  24870  hlcph  24881  minveclem4  24949  ivthlem3  24970  ovolmge0  24994  ovolicc1  25033  ovolicc2lem3  25036  ovolicc2lem5  25038  dyadmbl  25117  i1ff  25193  i1frn  25194  i1fima2  25196  itg2monolem1  25268  dvnres  25448  c1liplem1  25513  c1lip2  25515  dvge0  25523  lhop1lem  25530  itgsubstlem  25565  fta1glem2  25684  fta1b  25687  plyf  25712  plypf1  25726  plyadd  25731  plymul  25732  coeeu  25739  dgrlem  25743  coeid  25752  elqaalem3  25834  aareccl  25839  eff1olem  26057  relogf1o  26075  logdmn0  26148  logcnlem2  26151  logcnlem3  26152  efopnlem1  26164  efopnlem2  26165  logtayl2  26170  cxpcn3lem  26255  cxpcn3  26256  logbgcd1irr  26299  atandmneg  26411  atandmcj  26414  efiatan2  26422  cosatan  26426  cosatanne0  26427  dvatan  26440  areage0  26468  cxp2lim  26481  jensenlem2  26492  jensen  26493  eldmgm  26526  dmgmaddn0  26527  dmlogdmgm  26528  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem5  26537  lgambdd  26541  lgamucov  26542  ftalem3  26579  efnnfsumcl  26607  efchtdvds  26663  sqff1o  26686  fsumdvdsdiaglem  26687  dvdsppwf1o  26690  dvdsflf1o  26691  musum  26695  muinv  26697  dvdsmulf1o  26698  lgsfle1  26809  lgsle1  26815  lgsdirprm  26834  lgsne0  26838  lgseisenlem3  26880  lgseisenlem4  26881  lgsquadlem1  26883  lgsquadlem2  26884  chebbnd1  26975  chtppilim  26978  chpchtlim  26982  chpo1ub  26983  dchrmusumlema  26996  dchrvmasumlem1  26998  dchrisum0lema  27017  dchrisum0lem2a  27020  logsqvma  27045  selberg3lem2  27061  pntrsumo1  27068  pnt2  27116  ostthlem1  27130  ostth3  27141  sltval2  27159  addsproplem2  27454  sleadd1  27472  negsid  27515  precsexlem8  27660  precsexlem9  27661  precsexlem11  27663  axtgcgrrflx  27713  axtgcgrid  27714  axtgsegcon  27715  axtg5seg  27716  axtgbtwnid  27717  axtgpasch  27718  axtgcont1  27719  tglng  27797  axcontlem7  28228  axcontlem10  28231  upgrle  28350  umgredg2  28360  lfgredgge2  28384  usgredg2ALT  28450  usgr1vr  28512  usgrexmpledg  28519  upgrres1  28570  fusgrvtxfi  28576  vtxnbuvtx  28648  cusgrcplgr  28677  vdumgr0  28737  vtxdgoddnumeven  28810  trlres  28957  usgr2pth  29021  cyclispthon  29058  clwwlknlen  29285  clwwnonrepclwwnon  29598  2clwwlk2  29601  ablocom  29801  phpar2  30076  cbncms  30118  hlph  30142  hcaucvg  30439  hlimconvi  30444  shaddcl  30470  shmulcl  30471  chlimi  30487  chcompl  30495  choc1  30580  nmopre  31123  cnopc  31166  lnopl  31167  unop  31168  hmop  31175  cnfnc  31183  lnfnl  31184  nlelshi  31313  cnlnadjlem5  31324  elpjidm  31437  mdslle1i  31570  mdslle2i  31571  atcv0  31595  chpssati  31616  aciunf1lem  31887  padct  31944  ssnnssfz  31998  ccatf1  32115  swrdrndisj  32121  ressprs  32133  oduprs  32134  resspos  32136  resstos  32137  pwrssmgc  32170  ogrpinv0le  32233  ogrpsub  32234  ogrpaddlt  32235  cyc3evpm  32309  cycpmgcl  32312  cycpmconjslem2  32314  cyc3conja  32316  isarchi3  32333  archirng  32334  archirngz  32335  archiabllem1a  32337  archiabllem1b  32338  archiabllem2a  32340  archiabllem2c  32341  archiabllem2b  32342  archiabl  32344  isdrng4  32395  orngsqr  32422  ornglmulle  32423  orngrmulle  32424  ofldtos  32429  ofldlt1  32431  ofldchr  32432  suborng  32433  subofld  32434  isarchiofld  32435  nn0omnd  32460  quslsm  32516  nsgmgclem  32522  nsgmgc  32523  prmidl0  32569  qsidomlem1  32571  mxidlirred  32588  krull  32594  sradrng  32673  extdg1id  32742  ply1annnr  32764  madjusmdetlem4  32810  qtophaus  32816  crefi  32827  cmpcref  32830  cmppcmp  32838  pcmplfin  32840  zart0  32859  tpr2rico  32892  rge0scvg  32929  zrhunitpreima  32958  qqhrhm  32969  esummono  33052  gsumesum  33057  esumrnmpt2  33066  esumpinfval  33071  esumpcvgval  33076  esumpmono  33077  0elsiga  33112  sigaclcu  33115  issgon  33121  inelpisys  33152  ldsysgenld  33158  ldgenpisyslem1  33161  sxuni  33191  isrnmeas  33198  measvuni  33212  measssd  33213  ddemeas  33234  imambfm  33261  elmbfmvol2  33266  dya2icoseg2  33277  omssubaddlem  33298  omssubadd  33299  carsgsigalem  33314  pmeasmono  33323  sibfinima  33338  oddpwdc  33353  oddpwdcv  33354  eulerpartlemf  33369  eulerpartlemt  33370  eulerpartlemr  33373  eulerpartlemgvv  33375  eulerpartlemgs2  33379  fiblem  33397  probtot  33411  ballotlem4  33497  ballotlem5  33498  ballotlemfrc  33525  ballotlemirc  33530  ballotth  33536  hgt750lemb  33668  bnj642  33759  bnj643  33760  bnj645  33761  bnj707  33766  bnj1379  33841  bnj1538  33866  bnj110  33869  bnj93  33874  bnj906  33941  bnj1006  33971  bnj1110  33993  bnj1121  33996  bnj1204  34023  bnj1321  34038  bnj1364  34039  bnj1398  34045  bnj1450  34061  bnj1312  34069  bnj1501  34078  bnj1523  34082  0nn0m1nnn0  34102  subfacp1lem3  34173  subfacp1lem5  34175  pconncn  34215  connpconn  34226  cvmcov  34254  cvmliftlem1  34276  cvmliftlem10  34285  cvmlift2lem11  34304  cvmlift2lem12  34305  msubff1  34547  mvhf1  34550  mthmpps  34573  mclspps  34575  fundmpss  34738  funpartfun  34915  fnetg  35230  neibastop1  35244  filnetlem3  35265  onint1  35334  bj-nnfa  35606  bj-idres  36041  bj-rvecrr  36178  icorempo  36232  pibt2  36298  wl-nfeqfb  36405  phpreu  36472  fin2solem  36474  fin2so  36475  lindsenlbs  36483  matunitlindflem1  36484  matunitlindflem2  36485  matunitlindf  36486  ptrest  36487  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem26  36514  poimirlem27  36515  poimirlem29  36517  poimirlem31  36519  mblfinlem2  36526  dvtan  36538  itg2gt0cn  36543  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  cover2  36583  indexa  36601  istotbnd3  36639  sstotbnd2  36642  sstotbnd  36643  totbndss  36645  equivtotbnd  36646  isbnd3  36652  totbndbnd  36657  equivbnd  36658  prdsbnd  36661  prdstotbnd  36662  heibor  36689  zrdivrng  36821  crngocom  36869  isfld2  36873  dmncrng  36924  eqvrelrel  37467  disjrel  37600  disjdmqscossss  37673  prter2  37751  toycom  37843  lsateln0  37865  lpssat  37883  lssat  37886  oposlem  38052  olop  38084  omllaw  38113  cvlexch1  38198  dihpN  40207  mapdordlem2  40508  mhphflem  41168  prjspertr  41347  nacsfg  41443  nacsfix  41450  mzpindd  41484  diophrw  41497  diophrex  41513  rexzrexnn0  41542  pell1234qrdich  41599  rmspecnonsq  41645  rmspecfund  41647  rmspecpos  41655  monotoddzzfi  41681  ltrmxnn0  41688  rmxnn  41690  jm2.23  41735  jm3.1lem2  41757  dnnumch3  41789  lnmlssfg  41822  lnmlmic  41830  lnrlnm  41855  lnr2i  41858  lpirlnr  41859  hbtlem6  41871  hbt  41872  mnccoe  41880  idomrootle  41937  proot1mul  41941  proot1hash  41942  deg1mhm  41949  ondif1i  42012  limnsuc  42015  cantnfresb  42074  succlg  42078  ntrneifv2  42831  grucollcld  43019  mnurndlem1  43040  ismnushort  43060  radcnvrat  43073  binomcxplemdvbinom  43112  binomcxplemcvg  43113  binomcxplemnotnn0  43115  ordelordALT  43298  2uasbanh  43322  ordelordALTVD  43628  elixpconstg  43778  rabidim2  43791  foelrnf  43884  disjinfi  43891  supminfxr2  44179  sumnnodd  44346  stoweidlem7  44723  stoweidlem14  44730  stoweidlem16  44732  stoweidlem24  44740  stoweidlem31  44747  stoweidlem54  44770  wallispilem3  44783  fourierdlem42  44865  fourierdlem48  44870  fourierdlem51  44873  fourierdlem64  44886  fourierdlem76  44898  fourierdlem79  44901  fourierdlem81  44903  fourierdlem87  44909  etransclem28  44978  etransclem32  44982  sge0fodjrnlem  45132  hoidmvlelem3  45313  ovolval5lem3  45370  pimrecltpos  45424  pimrecltneg  45440  issmflem  45443  smfaddlem1  45479  smfsuplem1  45527  smfsuplem3  45529  smflimsuplem7  45542  smfliminflem  45546  tworepnotupword  45600  nfunsnafv  45850  faovcl  45908  tz6.12-2-afv2  45945  tz6.12i-afv2  45951  sprel  46152  evendiv2z  46300  oddp1div2z  46301  2dvdseven  46321  2ndvdsodd  46323  perfectALTVlem1  46389  sbgoldbm  46452  clintopcllaw  46621  0ringbas  46645  rnghmmgmhm  46692  2idlcpblrng  46766  uzlidlring  46827  rnghmsubcsetclem1  46873  rngccatidALTV  46887  zrinitorngc  46898  zrtermorngc  46899  rhmsubcsetclem1  46919  ringcinv  46930  funcringcsetcALTV2lem7  46940  ringccatidALTV  46950  ringcinvALTV  46954  funcringcsetclem7ALTV  46963  irinitoringc  46967  zrtermoringc  46968  fldhmsubc  46982  fldhmsubcALTV  47000  ssnn0ssfz  47025  el0ldepsnzr  47148  regt1loggt0  47222  elbigodm  47241  fllogbd  47246  rrx2xpref1o  47404  unilbss  47502  fdomne0  47516  f002  47520  thincmo2  47648  thincmoALT  47650  fullthinc  47666  elsetrecslem  47744