Theorem simprbi 497

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 496	1 ⊢ (𝜑 → 𝜒)

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

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 397

This theorem is referenced by:  simplbiim  505  xornan  1518  eumo  2572  reurmo  3379  pssne  4096  pssn2lp  4101  ssnpss  4103  eldifn  4127  elinel2  4196  rabsnt  4735  eldifsni  4793  unimax  4948  ssintub  4970  moop2  5502  pwssun  5571  weso  5667  opelxp2  5719  predpo  6324  frpoinsg  6344  wfisgOLD  6355  ordwe  6377  funmo  6563  funmoOLD  6564  funopg  6582  funun  6594  fununi  6623  funimaexg  6634  fndm  6652  frn  6724  f1ss  6793  f1ssr  6794  forn  6808  f1f1orn  6844  f1orescnv  6848  f1imacnv  6849  funcocnv2  6858  dffv2  6986  exfo  7106  foelrn  7108  foelrnf  7109  isorel  7325  isoini2  7338  f1ofveu  7405  fovcld  7538  onminesb  7783  onminsb  7784  tfisg  7845  tfis  7846  limomss  7862  nnlim  7871  ssnlim  7877  curry1  8092  curry2  8095  f1o2ndf1  8110  fnwelem  8119  mpoxopn0yelv  8200  wfrlem5OLD  8315  tz7.48lem  8443  dif20el  8507  oeordi  8589  oeeulem  8603  oeeui  8604  nnawordex  8639  swoer  8735  eceqoveq  8818  mapsnconst  8888  resixpfo  8932  boxcutc  8937  sdomnen  8979  en0  9015  en0OLD  9016  en0ALT  9017  en0r  9018  en1  9023  en1OLD  9024  dom0  9104  fodomr  9130  dif1enlem  9158  dif1enlemOLD  9159  unxpdomlem3  9254  fineqvlem  9264  infn0  9309  f1opwfi  9358  fsuppcolem  9398  fsuppco  9399  mapfienlem1  9402  mapfienlem2  9403  supub  9456  suplub  9457  ordtypelem2  9516  ordtypelem3  9517  ordtypelem6  9520  ordtypelem7  9521  wemapso2lem  9549  wdom2d  9577  brwdom3  9579  ixpiunwdom  9587  inf3lem2  9626  inf3lem6  9630  oancom  9648  infdifsn  9654  cantnfp1lem3  9677  cantnflem3  9688  cantnflem4  9689  oef1o  9695  cnfcom3  9701  tctr  9737  frinsg  9748  tz9.12lem3  9786  scottex  9882  cardid2  9950  infxpenlem  10010  acni3  10044  cardaleph  10086  iscard3  10090  dfac5lem4  10123  dfac5lem5  10124  kmlem1  10147  cofsmo  10266  fin4en1  10306  enfin2i  10318  fin23lem28  10337  fin23lem38  10346  isf32lem6  10355  enfin1ai  10381  hsmexlem2  10424  hsmexlem4  10426  domtriomlem  10439  axdc2lem  10445  axdc3lem2  10448  ac6num  10476  zorn2lem2  10494  brdom3  10525  alephval2  10569  alephreg  10579  pwcfsdom  10580  smobeth  10583  fpwwe2lem5  10632  fpwwe2lem12  10639  canthp1lem2  10650  pwfseqlem3  10657  hargch  10670  winalim2  10693  gchina  10696  inar1  10772  0npi  10879  mulclpi  10890  mulcanpi  10897  nlt1pi  10903  nqereu  10926  prcdnq  10990  prnmax  10992  ltresr2  11138  axrnegex  11159  axpre-sup  11166  eluz2gt1  12908  1nuz2  12912  zsupss  12925  rpgt0  12990  ixxss1  13346  ixxss2  13347  ixxss12  13348  lbioo  13359  ubioo  13360  iccss2  13399  iccssico2  13402  elfzuz3  13502  serge0  14026  expge0  14068  expge1  14069  expaddzlem  14075  hashrabsn1  14338  hashfun  14401  cshinj  14765  relexpuzrel  15003  shftfn  15024  01sqrexlem6  15198  rlimss  15450  lo1dm  15467  o1dm  15478  rlimrege0  15527  fsumf1o  15673  fsumge0  15745  incexc2  15788  supcvg  15806  fprodf1o  15894  divalglem9  16348  bitsfzolem  16379  bitsf1  16391  gcdcllem1  16444  bezout  16489  nprm  16629  dvdsprm  16644  coprm  16652  dfphi2  16711  phimullem  16716  phisum  16727  expnprm  16839  prmreclem2  16854  prmreclem5  16857  1arith  16864  4sqlem18  16899  vdwnnlem3  16934  ramtlecl  16937  rami  16952  0ram  16957  ramub1lem1  16963  prmgaplem5  16992  acsfiel  17602  isacs1i  17605  catlid  17631  catrid  17632  fullfo  17867  fthf1  17872  fthoppc  17878  invfuc  17931  prslem  18255  posi  18274  tleile  18378  dlatmjdi  18480  pslem  18529  tsrlin  18542  cnvtsr  18545  tsrdir  18561  mndid  18669  mhmf  18711  mhmlin  18715  mhm0  18716  mndind  18745  grpinvex  18865  grplinv  18910  mulgz  19018  mulgdirlem  19021  mulgdir  19022  mulgass  19027  nsgbi  19073  nmzbi  19080  ghmf  19134  ghmlin  19135  conjnsg  19168  gimf1o  19177  gagrpid  19199  gaf  19200  gaass  19202  psgnunilem5  19403  odid  19447  odf1o2  19482  gexid  19490  sylow1lem4  19510  pj1id  19608  efgredeu  19661  ablcmn  19696  cmncom  19707  mulgdi  19735  torsubg  19763  cyggenod2  19794  cygctb  19801  ghmcyg  19805  dprdf1o  19943  ablfacrplem  19976  ablfaclem2  19997  ablfac2  20000  simpg2nsg  20007  fincygsubgodexd  20024  crngmgp  20135  rnghmmgmhm  20334  rhmmhm  20370  rhmghm  20375  rimf1o  20385  nzrnz  20406  opprnzr  20411  0ringbas  20417  subrgss  20462  subrg1cl  20470  drngunit  20505  fldcrngd  20513  drngmgp  20516  drngid  20518  issubdrg  20544  fldsdrgfld  20557  cntzsdrg  20561  abvge0  20576  srngcnv  20604  lmhmlin  20790  lmimf1o  20818  lvecdrng  20860  lspsolvlem  20900  islbs3  20913  lbsextlem3  20918  2idlelbas  21019  2idlcpblrng  21020  rrgeq0i  21105  domneq0  21113  domnrrg  21116  drngdomn  21121  fldidomOLD  21124  zringunit  21237  prmirredlem  21243  znidomb  21336  cygzn  21345  psgndiflemB  21372  pjf  21487  frlmsslsp  21570  frlmlbs  21571  f1lindf  21596  assalem  21631  psrbaglefi  21704  mplelsfi  21773  mplsubrglem  21782  mplcoe1  21811  mplbas2  21816  opsrtoslem2  21836  mhpmulcl  21911  coe1mul2  22011  pmatcoe1fsupp  22423  toponuni  22636  tpsuni  22658  mretopd  22816  neips  22837  neiptoptop  22855  neiptopnei  22856  perflp  22878  perfi  22879  cnf  22970  cnpf  22971  cnpimaex  22980  cnima  22989  t0sep  23048  t1ficld  23051  hausnei  23052  pnrmcld  23066  cnrmi  23084  cmpcov  23113  tgcmp  23125  hauscmplem  23130  connclo  23139  1stcclb  23168  2ndcdisj  23180  llyi  23198  nllyi  23199  ptpjpre1  23295  ptpjcn  23335  ptpjopn  23336  ptclsg  23339  dfac14  23342  txdis1cn  23359  pthaus  23362  hauseqlcld  23370  txkgen  23376  xkococn  23384  txconn  23413  hmeocnvcn  23485  fbssfi  23561  filss  23577  uffixfr  23647  flimneiss  23690  flimelbas  23692  flimfnfcls  23752  alexsubb  23770  alexsubALT  23775  ptcmplem2  23777  ptcmplem3  23778  ptcmplem4  23779  tmdgsum2  23820  ghmcnp  23839  tgpt0  23843  qustgplem  23845  istdrg2  23902  vscacn  23910  tvctdrg  23917  uspreg  23999  ucncn  24010  neipcfilu  24021  cuspcvg  24026  psmetxrge0  24039  isxmet2d  24053  prdsxmetlem  24094  imasdsf1olem  24099  xmstopn  24177  mstopn  24178  stdbdxmet  24244  prdsxmslem2  24258  nrgabv  24398  nmvs  24413  nvclvec  24434  nmoge0  24458  nghmcl  24464  nmoi  24465  nghmghm  24471  nmhmlmhm  24486  nmhmnghm  24487  icccmp  24561  xrge0gsumle  24569  metds0  24586  metdstri  24587  metdsre  24589  metdseq0  24590  metdscnlem  24591  metnrmlem1a  24594  icopnfcnv  24682  xrhmeo  24686  pcoval1  24753  cvslvec  24865  cvsunit  24871  recvs  24886  cphreccllem  24919  cphsscph  24992  cmetcvg  25026  lmle  25042  cmscmet  25087  cmetcusp1  25094  hlcph  25105  minveclem4  25173  ivthlem3  25194  ovolmge0  25218  ovolicc1  25257  ovolicc2lem3  25260  ovolicc2lem5  25262  dyadmbl  25341  i1ff  25417  i1frn  25418  i1fima2  25420  itg2monolem1  25492  dvnres  25672  c1liplem1  25737  c1lip2  25739  dvge0  25747  lhop1lem  25754  itgsubstlem  25789  fta1glem2  25908  fta1b  25911  plyf  25936  plypf1  25950  plyadd  25955  plymul  25956  coeeu  25963  dgrlem  25967  coeid  25976  elqaalem3  26058  aareccl  26063  eff1olem  26281  relogf1o  26299  logdmn0  26372  logcnlem2  26375  logcnlem3  26376  efopnlem1  26388  efopnlem2  26389  logtayl2  26394  cxpcn3lem  26479  cxpcn3  26480  logbgcd1irr  26523  atandmneg  26635  atandmcj  26638  efiatan2  26646  cosatan  26650  cosatanne0  26651  dvatan  26664  areage0  26692  cxp2lim  26705  jensenlem2  26716  jensen  26717  eldmgm  26750  dmgmaddn0  26751  dmlogdmgm  26752  lgamgulmlem2  26758  lgamgulmlem3  26759  lgamgulmlem5  26761  lgambdd  26765  lgamucov  26766  ftalem3  26803  efnnfsumcl  26831  efchtdvds  26887  sqff1o  26910  fsumdvdsdiaglem  26911  dvdsppwf1o  26914  dvdsflf1o  26915  musum  26919  muinv  26921  dvdsmulf1o  26922  lgsfle1  27033  lgsle1  27039  lgsdirprm  27058  lgsne0  27062  lgseisenlem3  27104  lgseisenlem4  27105  lgsquadlem1  27107  lgsquadlem2  27108  chebbnd1  27199  chtppilim  27202  chpchtlim  27206  chpo1ub  27207  dchrmusumlema  27220  dchrvmasumlem1  27222  dchrisum0lema  27241  dchrisum0lem2a  27244  logsqvma  27269  selberg3lem2  27285  pntrsumo1  27292  pnt2  27340  ostthlem1  27354  ostth3  27365  sltval2  27383  addsproplem2  27680  sleadd1  27699  negsid  27742  precsexlem8  27887  precsexlem9  27888  precsexlem11  27890  elons2  27912  sltonold  27914  onscutleft  27916  axtgcgrrflx  27968  axtgcgrid  27969  axtgsegcon  27970  axtg5seg  27971  axtgbtwnid  27972  axtgpasch  27973  axtgcont1  27974  tglng  28052  axcontlem7  28483  axcontlem10  28486  upgrle  28605  umgredg2  28615  lfgredgge2  28639  usgredg2ALT  28705  usgr1vr  28767  usgrexmpledg  28774  upgrres1  28825  fusgrvtxfi  28831  vtxnbuvtx  28903  cusgrcplgr  28932  vdumgr0  28992  vtxdgoddnumeven  29065  trlres  29212  usgr2pth  29276  cyclispthon  29313  clwwlknlen  29540  clwwnonrepclwwnon  29853  2clwwlk2  29856  ablocom  30056  phpar2  30331  cbncms  30373  hlph  30397  hcaucvg  30694  hlimconvi  30699  shaddcl  30725  shmulcl  30726  chlimi  30742  chcompl  30750  choc1  30835  nmopre  31378  cnopc  31421  lnopl  31422  unop  31423  hmop  31430  cnfnc  31438  lnfnl  31439  nlelshi  31568  cnlnadjlem5  31579  elpjidm  31692  mdslle1i  31825  mdslle2i  31826  atcv0  31850  chpssati  31871  aciunf1lem  32142  padct  32199  ssnnssfz  32253  ccatf1  32370  swrdrndisj  32376  ressprs  32388  oduprs  32389  resspos  32391  resstos  32392  pwrssmgc  32425  ogrpinv0le  32491  ogrpsub  32492  ogrpaddlt  32493  cyc3evpm  32567  cycpmgcl  32570  cycpmconjslem2  32572  cyc3conja  32574  isarchi3  32591  archirng  32592  archirngz  32593  archiabllem1a  32595  archiabllem1b  32596  archiabllem2a  32598  archiabllem2c  32599  archiabllem2b  32600  archiabl  32602  isdrng4  32653  orngsqr  32680  ornglmulle  32681  orngrmulle  32682  ofldtos  32687  ofldlt1  32689  ofldchr  32690  suborng  32691  subofld  32692  isarchiofld  32693  nn0omnd  32718  quslsm  32778  nsgmgclem  32784  nsgmgc  32785  prmidl0  32831  qsidomlem1  32833  mxidlirred  32850  krull  32856  sradrng  32946  extdg1id  33018  ply1annnr  33041  madjusmdetlem4  33096  qtophaus  33102  crefi  33113  cmpcref  33116  cmppcmp  33124  pcmplfin  33126  zart0  33145  tpr2rico  33178  rge0scvg  33215  zrhunitpreima  33244  qqhrhm  33255  esummono  33338  gsumesum  33343  esumrnmpt2  33352  esumpinfval  33357  esumpcvgval  33362  esumpmono  33363  0elsiga  33398  sigaclcu  33401  issgon  33407  inelpisys  33438  ldsysgenld  33444  ldgenpisyslem1  33447  sxuni  33477  isrnmeas  33484  measvuni  33498  measssd  33499  ddemeas  33520  imambfm  33547  elmbfmvol2  33552  dya2icoseg2  33563  omssubaddlem  33584  omssubadd  33585  carsgsigalem  33600  pmeasmono  33609  sibfinima  33624  oddpwdc  33639  oddpwdcv  33640  eulerpartlemf  33655  eulerpartlemt  33656  eulerpartlemr  33659  eulerpartlemgvv  33661  eulerpartlemgs2  33665  fiblem  33683  probtot  33697  ballotlem4  33783  ballotlem5  33784  ballotlemfrc  33811  ballotlemirc  33816  ballotth  33822  hgt750lemb  33954  bnj642  34045  bnj643  34046  bnj645  34047  bnj707  34052  bnj1379  34127  bnj1538  34152  bnj110  34155  bnj93  34160  bnj906  34227  bnj1006  34257  bnj1110  34279  bnj1121  34282  bnj1204  34309  bnj1321  34324  bnj1364  34325  bnj1398  34331  bnj1450  34347  bnj1312  34355  bnj1501  34364  bnj1523  34368  0nn0m1nnn0  34388  subfacp1lem3  34459  subfacp1lem5  34461  pconncn  34501  connpconn  34512  cvmcov  34540  cvmliftlem1  34562  cvmliftlem10  34571  cvmlift2lem11  34590  cvmlift2lem12  34591  msubff1  34833  mvhf1  34836  mthmpps  34859  mclspps  34861  fundmpss  35030  funpartfun  35207  fnetg  35533  neibastop1  35547  filnetlem3  35568  onint1  35637  bj-nnfa  35909  bj-idres  36344  bj-rvecrr  36481  icorempo  36535  pibt2  36601  wl-nfeqfb  36708  phpreu  36775  fin2solem  36777  fin2so  36778  lindsenlbs  36786  matunitlindflem1  36787  matunitlindflem2  36788  matunitlindf  36789  ptrest  36790  poimirlem1  36792  poimirlem2  36793  poimirlem3  36794  poimirlem4  36795  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem9  36800  poimirlem10  36801  poimirlem11  36802  poimirlem12  36803  poimirlem13  36804  poimirlem14  36805  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem18  36809  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem23  36814  poimirlem24  36815  poimirlem26  36817  poimirlem27  36818  poimirlem29  36820  poimirlem31  36822  mblfinlem2  36829  dvtan  36841  itg2gt0cn  36846  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  cover2  36886  indexa  36904  istotbnd3  36942  sstotbnd2  36945  sstotbnd  36946  totbndss  36948  equivtotbnd  36949  isbnd3  36955  totbndbnd  36960  equivbnd  36961  prdsbnd  36964  prdstotbnd  36965  heibor  36992  zrdivrng  37124  crngocom  37172  isfld2  37176  dmncrng  37227  eqvrelrel  37770  disjrel  37903  disjdmqscossss  37976  prter2  38054  toycom  38146  lsateln0  38168  lpssat  38186  lssat  38189  oposlem  38355  olop  38387  omllaw  38416  cvlexch1  38501  dihpN  40510  mapdordlem2  40811  mhphflem  41470  prjspertr  41649  nacsfg  41745  nacsfix  41752  mzpindd  41786  diophrw  41799  diophrex  41815  rexzrexnn0  41844  pell1234qrdich  41901  rmspecnonsq  41947  rmspecfund  41949  rmspecpos  41957  monotoddzzfi  41983  ltrmxnn0  41990  rmxnn  41992  jm2.23  42037  jm3.1lem2  42059  dnnumch3  42091  lnmlssfg  42124  lnmlmic  42132  lnrlnm  42157  lnr2i  42160  lpirlnr  42161  hbtlem6  42173  hbt  42174  mnccoe  42182  idomrootle  42239  proot1mul  42243  proot1hash  42244  deg1mhm  42251  ondif1i  42314  limnsuc  42317  cantnfresb  42376  succlg  42380  ntrneifv2  43133  grucollcld  43321  mnurndlem1  43342  ismnushort  43362  radcnvrat  43375  binomcxplemdvbinom  43414  binomcxplemcvg  43415  binomcxplemnotnn0  43417  ordelordALT  43600  2uasbanh  43624  ordelordALTVD  43930  elixpconstg  44080  rabidim2  44093  disjinfi  44190  supminfxr2  44478  sumnnodd  44645  stoweidlem7  45022  stoweidlem14  45029  stoweidlem16  45031  stoweidlem24  45039  stoweidlem31  45046  stoweidlem54  45069  wallispilem3  45082  fourierdlem42  45164  fourierdlem48  45169  fourierdlem51  45172  fourierdlem64  45185  fourierdlem76  45197  fourierdlem79  45200  fourierdlem81  45202  fourierdlem87  45208  etransclem28  45277  etransclem32  45281  sge0fodjrnlem  45431  hoidmvlelem3  45612  ovolval5lem3  45669  pimrecltpos  45723  pimrecltneg  45739  issmflem  45742  smfaddlem1  45778  smfsuplem1  45826  smfsuplem3  45828  smflimsuplem7  45841  smfliminflem  45845  tworepnotupword  45899  nfunsnafv  46149  faovcl  46207  tz6.12-2-afv2  46244  tz6.12i-afv2  46250  sprel  46451  evendiv2z  46599  oddp1div2z  46600  2dvdseven  46620  2ndvdsodd  46622  perfectALTVlem1  46688  sbgoldbm  46751  clintopcllaw  46888  uzlidlring  46916  rnghmsubcsetclem1  46962  rngccatidALTV  46976  zrinitorngc  46987  zrtermorngc  46988  rhmsubcsetclem1  47008  ringcinv  47019  funcringcsetcALTV2lem7  47029  ringccatidALTV  47039  ringcinvALTV  47043  funcringcsetclem7ALTV  47052  irinitoringc  47056  zrtermoringc  47057  fldhmsubc  47071  fldhmsubcALTV  47089  ssnn0ssfz  47114  el0ldepsnzr  47236  regt1loggt0  47310  elbigodm  47329  fllogbd  47334  rrx2xpref1o  47492  unilbss  47590  fdomne0  47604  f002  47608  thincmo2  47736  thincmoALT  47738  fullthinc  47754  elsetrecslem  47832